Charlie is big. Charlie is blue. Charlie is quiet. Erin is blue. Erin is cold. Erin is quiet. Erin is smart. Fiona is big. Fiona is blue. Fiona is cold. Fiona is nice. Fiona is smart. Harry is cold. Harry is nice. Harry is rough. Harry is smart. If Harry is quiet then Harry is cold. If someone is cold and smart then they are quiet. All rough people are nice. Blue people are rough. Big, nice people are cold. All quiet, big people are smart.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If Harry is quiet then Harry is cold.
((("Harry" "is" "quiet" "+")) -> ("Harry" "is" "cold" "+"))
If someone is cold and smart then they are quiet.
((("someone" "is" "cold" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "quiet" "+"))
All rough people are nice.
((("someone" "is" "rough" "+")) -> ("someone" "is" "nice" "+"))
Blue people are rough.
((("someone" "is" "blue" "+")) -> ("someone" "is" "rough" "+"))
Big, nice people are cold.
((("someone" "is" "big" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "cold" "+"))
All quiet, big people are smart.
((("someone" "is" "quiet" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "smart" "+"))
Harry is smart.
True
1
proof
[(triple16)]
("Harry" "is" "smart" "+")
triple16
Charlie is not blue.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "blue" "-")
triple2
Fiona is quiet.
True
3
proof
[(((triple10 triple12) -> rule2) OR ((((triple8 triple11) -> rule5) triple12) -> rule2) OR ((((triple8 ((((triple9) -> rule4)) -> rule3)) -> rule5) triple12) -> rule2))]
("Fiona" "is" "quiet" "+")
((triple10 triple12) -> (rule2 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
((((triple8 triple11) -> (rule5 % int2)) triple12) -> (rule2 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
((((triple8 ((((triple9) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule5 % int2)) triple12) -> (rule2 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
int3
Fiona is rough.
("Fiona" "is" "rough" "+")
int4
Charlie is not rough.
False
2
inv-proof
[(((triple2) -> rule4))]
("Charlie" "is" "rough" "-")
((triple2) -> (rule4 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Erin is nice.
True
3
proof
[(((((triple4) -> rule4)) -> rule3))]
("Erin" "is" "nice" "+")
((((triple4) -> (rule4 % int2))) -> (rule3 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is not nice.
False
3
inv-proof
[(((((triple4) -> rule4)) -> rule3))]
("Erin" "is" "nice" "-")
((((triple4) -> (rule4 % int2))) -> (rule3 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Charlie is cold.
True
5
proof
[(((triple1 ((((triple2) -> rule4)) -> rule3)) -> rule5))]
("Charlie" "is" "cold" "+")
((triple1 ((((triple2) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is not cold.
False
5
inv-proof
[(((triple1 ((((triple2) -> rule4)) -> rule3)) -> rule5))]
("Charlie" "is" "cold" "-")
((triple1 ((((triple2) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Erin is not big.
Unknown
inv-random
[@0: Erin is big.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "big" "-")
Harry is blue.
Unknown
random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "+")
@0: Charlie is big.[(triple1)] Charlie is blue.[(triple2)] Charlie is quiet.[(triple3)] Erin is blue.[(triple4)] Erin is cold.[(triple5)] Erin is quiet.[(triple6 OR ((triple5 triple7) -> rule2))] Erin is smart.[(triple7)] Fiona is big.[(triple8)] Fiona is blue.[(triple9)] Fiona is cold.[(triple10 OR ((triple8 triple11) -> rule5) OR ((triple8 ((((triple9) -> rule4)) -> rule3)) -> rule5))] Fiona is nice.[(triple11 OR ((((triple9) -> rule4)) -> rule3))] Fiona is smart.[(triple12)] Harry is cold.[(triple13)] Harry is nice.[(triple14 OR ((triple15) -> rule3))] Harry is rough.[(triple15)] Harry is smart.[(triple16)] @1: Charlie is rough.[(((triple2) -> rule4))] Charlie is smart.[(((triple3 triple1) -> rule6))] Erin is rough.[(((triple4) -> rule4))] Fiona is quiet.[(((triple10 triple12) -> rule2) OR ((((triple8 triple11) -> rule5) triple12) -> rule2) OR ((((triple8 ((((triple9) -> rule4)) -> rule3)) -> rule5) triple12) -> rule2))] Fiona is rough.[(((triple9) -> rule4))] Harry is quiet.[(((triple13 triple16) -> rule2))] @2: Charlie is nice.[(((((triple2) -> rule4)) -> rule3))] Erin is nice.[(((((triple4) -> rule4)) -> rule3))] @3: Charlie is cold.[(((triple1 ((((triple2) -> rule4)) -> rule3)) -> rule5))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Charlie is blue.
("Charlie" "is" "blue" "+")
triple2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple3
Erin is blue.
("Erin" "is" "blue" "+")
triple4
Erin is cold.
("Erin" "is" "cold" "+")
triple5
Erin is quiet.
("Erin" "is" "quiet" "+")
triple6
((triple5 triple7) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
triple7
Fiona is big.
("Fiona" "is" "big" "+")
triple8
Fiona is blue.
("Fiona" "is" "blue" "+")
triple9
Fiona is cold.
("Fiona" "is" "cold" "+")
triple10
((triple8 triple11) -> (rule5 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
((triple8 ((((triple9) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
int3
Fiona is nice.
("Fiona" "is" "nice" "+")
triple11
((((triple9) -> (rule4 % int2))) -> (rule3 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
triple12
Harry is cold.
("Harry" "is" "cold" "+")
triple13
Harry is nice.
("Harry" "is" "nice" "+")
triple14
((triple15) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
triple15
Harry is smart.
("Harry" "is" "smart" "+")
triple16
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple2) -> (rule4 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple3 triple1) -> (rule6 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
((triple4) -> (rule4 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((triple10 triple12) -> (rule2 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
((((triple8 triple11) -> (rule5 % int2)) triple12) -> (rule2 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
((((triple8 ((((triple9) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule5 % int2)) triple12) -> (rule2 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
int3
Fiona is rough.
("Fiona" "is" "rough" "+")
int4
Fiona is rough.
("Fiona" "is" "rough" "+")
((triple9) -> (rule4 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple13 triple16) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
((((triple2) -> (rule4 % int2))) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
((((triple4) -> (rule4 % int2))) -> (rule3 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
((triple1 ((((triple2) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3