Fiona is cold. Fiona is not kind. Fiona is nice. Fiona is quiet. Fiona is red. Fiona is not rough. Fiona is young. Harry is cold. Harry is quiet. Harry is red. All young things are nice. All red, kind things are nice. All kind, quiet things are cold. If something is nice then it is red. If something is kind and not quiet then it is young. All cold things are young. All nice things are not kind. If something is kind and not young then it is rough.
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is not kind.
("Fiona" "is" "kind" "-")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Fiona is not rough.
("Fiona" "is" "rough" "-")
Fiona is young.
("Fiona" "is" "young" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is red.
("Harry" "is" "red" "+")
All young things are nice.
((("something" "is" "young" "+")) -> ("something" "is" "nice" "+"))
All red, kind things are nice.
((("something" "is" "red" "+") ("something" "is" "kind" "+")) -> ("something" "is" "nice" "+"))
All kind, quiet things are cold.
((("something" "is" "kind" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "cold" "+"))
If something is nice then it is red.
((("something" "is" "nice" "+")) -> ("something" "is" "red" "+"))
If something is kind and not quiet then it is young.
((("something" "is" "kind" "+") ("something" "is" "quiet" "~")) -> ("something" "is" "young" "+"))
All cold things are young.
((("something" "is" "cold" "+")) -> ("something" "is" "young" "+"))
All nice things are not kind.
((("something" "is" "nice" "+")) -> ("something" "is" "kind" "-"))
If something is kind and not young then it is rough.
((("something" "is" "kind" "+") ("something" "is" "young" "~")) -> ("something" "is" "rough" "+"))
Fiona is not kind.
True
1
proof
[(triple2 OR ((triple3) -> rule7) OR ((((triple7) -> rule1)) -> rule7) OR ((((((triple1) -> rule6)) -> rule1)) -> rule7))]
("Fiona" "is" "kind" "-")
triple2
((triple3) -> (rule7 % int1))
Fiona is not kind.
("Fiona" "is" "kind" "-")
int1
((((triple7) -> (rule1 % int2))) -> (rule7 % int1))
Fiona is not kind.
("Fiona" "is" "kind" "-")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
((((((triple1) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Fiona is not kind.
("Fiona" "is" "kind" "-")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Fiona is not red.
False
1
inv-proof
[(triple5 OR ((triple3) -> rule4) OR ((((triple7) -> rule1)) -> rule4) OR ((((((triple1) -> rule6)) -> rule1)) -> rule4))]
("Fiona" "is" "red" "-")
triple5
((triple3) -> (rule4 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
((((triple7) -> (rule1 % int2))) -> (rule4 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
((((((triple1) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Harry is young.
True
2
proof
[(((triple8) -> rule6))]
("Harry" "is" "young" "+")
((triple8) -> (rule6 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is not young.
False
2
inv-proof
[(((triple8) -> rule6))]
("Harry" "is" "young" "-")
((triple8) -> (rule6 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is nice.
True
3
proof
[(((((triple8) -> rule6)) -> rule1))]
("Harry" "is" "nice" "+")
((((triple8) -> (rule6 % int2))) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is not nice.
False
3
inv-proof
[(((((triple8) -> rule6)) -> rule1))]
("Harry" "is" "nice" "-")
((((triple8) -> (rule6 % int2))) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
@0: Fiona is cold.[(triple1)] Fiona is nice.[(triple3 OR ((triple7) -> rule1) OR ((((triple1) -> rule6)) -> rule1))] Fiona is not kind.[(triple2 OR ((triple3) -> rule7) OR ((((triple7) -> rule1)) -> rule7) OR ((((((triple1) -> rule6)) -> rule1)) -> rule7))] Fiona is not rough.[(triple6)] Fiona is quiet.[(triple4)] Fiona is red.[(triple5 OR ((triple3) -> rule4) OR ((((triple7) -> rule1)) -> rule4) OR ((((((triple1) -> rule6)) -> rule1)) -> rule4))] Fiona is young.[(triple7 OR ((triple1) -> rule6))] Harry is cold.[(triple8)] Harry is quiet.[(triple9)] Harry is red.[(triple10 OR ((((((triple8) -> rule6)) -> rule1)) -> rule4))] @1: Harry is young.[(((triple8) -> rule6))] @2: Harry is nice.[(((((triple8) -> rule6)) -> rule1))] @3: Harry is not kind.[(((((((triple8) -> rule6)) -> rule1)) -> rule7))]
Fiona is cold.
("Fiona" "is" "cold" "+")
triple1
Fiona is nice.
("Fiona" "is" "nice" "+")
triple3
((triple7) -> (rule1 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
((((triple1) -> (rule6 % int2))) -> (rule1 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is not kind.
("Fiona" "is" "kind" "-")
triple2
((triple3) -> (rule7 % int1))
Fiona is not kind.
("Fiona" "is" "kind" "-")
int1
((((triple7) -> (rule1 % int2))) -> (rule7 % int1))
Fiona is not kind.
("Fiona" "is" "kind" "-")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
((((((triple1) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Fiona is not kind.
("Fiona" "is" "kind" "-")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Fiona is not rough.
("Fiona" "is" "rough" "-")
triple6
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple4
Fiona is red.
("Fiona" "is" "red" "+")
triple5
((triple3) -> (rule4 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
((((triple7) -> (rule1 % int2))) -> (rule4 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
((((((triple1) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Fiona is young.
("Fiona" "is" "young" "+")
triple7
((triple1) -> (rule6 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
triple8
Harry is quiet.
("Harry" "is" "quiet" "+")
triple9
Harry is red.
("Harry" "is" "red" "+")
triple10
((((((triple8) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Harry is young.
("Harry" "is" "young" "+")
((triple8) -> (rule6 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
((((triple8) -> (rule6 % int2))) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is not kind.
("Harry" "is" "kind" "-")
((((((triple8) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Harry is not kind.
("Harry" "is" "kind" "-")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3