Erin is cold. Erin is red. Erin is rough. Erin is round. Fiona is blue. Fiona is cold. Fiona is quiet. Fiona is red. Fiona is rough. Fiona is young. Harry is blue. Harry is red. Harry is rough. Harry is round. Harry is young. If something is young then it is red. All young things are cold. If Harry is rough then Harry is quiet. All blue, cold things are red. If Fiona is quiet then Fiona is young. If Harry is cold then Harry is round.
Erin is cold.
("Erin" "is" "cold" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is round.
("Erin" "is" "round" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Fiona is young.
("Fiona" "is" "young" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is young.
("Harry" "is" "young" "+")
If something is young then it is red.
((("something" "is" "young" "+")) -> ("something" "is" "red" "+"))
All young things are cold.
((("something" "is" "young" "+")) -> ("something" "is" "cold" "+"))
If Harry is rough then Harry is quiet.
((("Harry" "is" "rough" "+")) -> ("Harry" "is" "quiet" "+"))
All blue, cold things are red.
((("something" "is" "blue" "+") ("something" "is" "cold" "+")) -> ("something" "is" "red" "+"))
If Fiona is quiet then Fiona is young.
((("Fiona" "is" "quiet" "+")) -> ("Fiona" "is" "young" "+"))
If Harry is cold then Harry is round.
((("Harry" "is" "cold" "+")) -> ("Harry" "is" "round" "+"))
Harry is red.
True
1
proof
[(triple12 OR ((triple15) -> rule1) OR ((triple11 ((triple15) -> rule2)) -> rule4))]
("Harry" "is" "red" "+")
triple12
((triple15) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
((triple11 ((triple15) -> (rule2 % int2))) -> (rule4 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is not rough.
False
1
inv-proof
[(triple13)]
("Harry" "is" "rough" "-")
triple13
Harry is quiet.
True
2
proof
[(((triple13) -> rule3))]
("Harry" "is" "quiet" "+")
((triple13) -> (rule3 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is not cold.
False
2
inv-proof
[(((triple15) -> rule2))]
("Harry" "is" "cold" "-")
((triple15) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Erin is not young.
Unknown
inv-random
[@0: Erin is young.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "young" "-")
Erin is blue.
Unknown
random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "+")
Erin is not quiet.
Unknown
inv-random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "-")
Fiona is round.
Unknown
random
[@0: Fiona is round.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "round" "+")
@0: Erin is cold.[(triple1)] Erin is red.[(triple2)] Erin is rough.[(triple3)] Erin is round.[(triple4)] Fiona is blue.[(triple5)] Fiona is cold.[(triple6 OR ((triple10) -> rule2) OR ((((triple7) -> rule5)) -> rule2))] Fiona is quiet.[(triple7)] Fiona is red.[(triple8 OR ((triple10) -> rule1) OR ((triple5 triple6) -> rule4) OR ((((triple7) -> rule5)) -> rule1) OR ((triple5 ((triple10) -> rule2)) -> rule4) OR ((triple5 ((((triple7) -> rule5)) -> rule2)) -> rule4))] Fiona is rough.[(triple9)] Fiona is young.[(triple10 OR ((triple7) -> rule5))] Harry is blue.[(triple11)] Harry is red.[(triple12 OR ((triple15) -> rule1) OR ((triple11 ((triple15) -> rule2)) -> rule4))] Harry is rough.[(triple13)] Harry is round.[(triple14 OR ((((triple15) -> rule2)) -> rule6))] Harry is young.[(triple15)] @1: Harry is cold.[(((triple15) -> rule2))] Harry is quiet.[(((triple13) -> rule3))]
Erin is cold.
("Erin" "is" "cold" "+")
triple1
Erin is red.
("Erin" "is" "red" "+")
triple2
Erin is rough.
("Erin" "is" "rough" "+")
triple3
Erin is round.
("Erin" "is" "round" "+")
triple4
Fiona is blue.
("Fiona" "is" "blue" "+")
triple5
Fiona is cold.
("Fiona" "is" "cold" "+")
triple6
((triple10) -> (rule2 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
((((triple7) -> (rule5 % int2))) -> (rule2 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple7
Fiona is red.
("Fiona" "is" "red" "+")
triple8
((triple10) -> (rule1 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
((triple5 triple6) -> (rule4 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
((((triple7) -> (rule5 % int2))) -> (rule1 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
((triple5 ((triple10) -> (rule2 % int2))) -> (rule4 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
((triple5 ((((triple7) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Fiona is rough.
("Fiona" "is" "rough" "+")
triple9
Fiona is young.
("Fiona" "is" "young" "+")
triple10
((triple7) -> (rule5 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
triple11
Harry is red.
("Harry" "is" "red" "+")
triple12
((triple15) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
((triple11 ((triple15) -> (rule2 % int2))) -> (rule4 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
triple13
Harry is round.
("Harry" "is" "round" "+")
triple14
((((triple15) -> (rule2 % int2))) -> (rule6 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
triple15
Harry is cold.
("Harry" "is" "cold" "+")
((triple15) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple13) -> (rule3 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1