Charlie is not cold. Fiona is smart. Gary is cold. Gary is kind. Gary is round. Harry is cold. Harry is kind. Harry is rough. Harry is round. Harry is smart. If something is cold then it is rough. Round things are blue. If Harry is smart then Harry is blue. If Harry is cold and Harry is quiet then Harry is round. All smart things are cold. Cold things are round. Blue things are quiet. All smart, quiet things are kind.
Charlie is not cold.
("Charlie" "is" "cold" "-")
Fiona is smart.
("Fiona" "is" "smart" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is round.
("Gary" "is" "round" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If something is cold then it is rough.
((("something" "is" "cold" "+")) -> ("something" "is" "rough" "+"))
Round things are blue.
((("something" "is" "round" "+")) -> ("something" "is" "blue" "+"))
If Harry is smart then Harry is blue.
((("Harry" "is" "smart" "+")) -> ("Harry" "is" "blue" "+"))
If Harry is cold and Harry is quiet then Harry is round.
((("Harry" "is" "cold" "+") ("Harry" "is" "quiet" "+")) -> ("Harry" "is" "round" "+"))
All smart things are cold.
((("something" "is" "smart" "+")) -> ("something" "is" "cold" "+"))
Cold things are round.
((("something" "is" "cold" "+")) -> ("something" "is" "round" "+"))
Blue things are quiet.
((("something" "is" "blue" "+")) -> ("something" "is" "quiet" "+"))
All smart, quiet things are kind.
((("something" "is" "smart" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "kind" "+"))
Harry is kind.
True
1
proof
[(triple7 OR ((triple10 ((((triple10) -> rule3)) -> rule7)) -> rule8) OR ((triple10 ((((triple9) -> rule2)) -> rule7)) -> rule8) OR ((triple10 ((((((triple6) -> rule6)) -> rule2)) -> rule7)) -> rule8) OR ((triple10 ((((((((triple10) -> rule5)) -> rule6)) -> rule2)) -> rule7)) -> rule8))]
("Harry" "is" "kind" "+")
triple7
((triple10 ((((triple10) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
((triple10 ((((triple9) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
((triple10 ((((((triple6) -> (rule6 % int4))) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is round.
("Harry" "is" "round" "+")
int4
((triple10 ((((((((triple10) -> (rule5 % int5))) -> (rule6 % int4))) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is round.
("Harry" "is" "round" "+")
int4
Harry is cold.
("Harry" "is" "cold" "+")
int5
Gary is not cold.
False
1
inv-proof
[(triple3)]
("Gary" "is" "cold" "-")
triple3
Harry is blue.
True
2
proof
[(((triple10) -> rule3) OR ((triple9) -> rule2) OR ((((triple6) -> rule6)) -> rule2) OR ((((((triple10) -> rule5)) -> rule6)) -> rule2))]
("Harry" "is" "blue" "+")
((triple10) -> (rule3 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
((triple9) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
((((triple6) -> (rule6 % int2))) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
((((((triple10) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Gary is not blue.
False
2
inv-proof
[(((triple5) -> rule2) OR ((((triple3) -> rule6)) -> rule2))]
("Gary" "is" "blue" "-")
((triple5) -> (rule2 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
((((triple3) -> (rule6 % int2))) -> (rule2 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Fiona is rough.
True
3
proof
[(((((triple2) -> rule5)) -> rule1))]
("Fiona" "is" "rough" "+")
((((triple2) -> (rule5 % int2))) -> (rule1 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Gary is not quiet.
False
3
inv-proof
[(((((triple5) -> rule2)) -> rule7) OR ((((((triple3) -> rule6)) -> rule2)) -> rule7))]
("Gary" "is" "quiet" "-")
((((triple5) -> (rule2 % int2))) -> (rule7 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
((((((triple3) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Fiona is blue.
True
4
proof
[(((((((triple2) -> rule5)) -> rule6)) -> rule2))]
("Fiona" "is" "blue" "+")
((((((triple2) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3
Fiona is not blue.
False
4
inv-proof
[(((((((triple2) -> rule5)) -> rule6)) -> rule2))]
("Fiona" "is" "blue" "-")
((((((triple2) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3
Fiona is quiet.
True
5
proof
[(((((((((triple2) -> rule5)) -> rule6)) -> rule2)) -> rule7))]
("Fiona" "is" "quiet" "+")
((((((((triple2) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
int3
Fiona is cold.
("Fiona" "is" "cold" "+")
int4
Fiona is not quiet.
False
5
inv-proof
[(((((((((triple2) -> rule5)) -> rule6)) -> rule2)) -> rule7))]
("Fiona" "is" "quiet" "-")
((((((((triple2) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
int3
Fiona is cold.
("Fiona" "is" "cold" "+")
int4
Fiona is kind.
True
7
proof
[(((triple2 ((((((((triple2) -> rule5)) -> rule6)) -> rule2)) -> rule7)) -> rule8))]
("Fiona" "is" "kind" "+")
((triple2 ((((((((triple2) -> (rule5 % int5))) -> (rule6 % int4))) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
Fiona is round.
("Fiona" "is" "round" "+")
int4
Fiona is cold.
("Fiona" "is" "cold" "+")
int5
Fiona is not kind.
False
7
inv-proof
[(((triple2 ((((((((triple2) -> rule5)) -> rule6)) -> rule2)) -> rule7)) -> rule8))]
("Fiona" "is" "kind" "-")
((triple2 ((((((((triple2) -> (rule5 % int5))) -> (rule6 % int4))) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
Fiona is round.
("Fiona" "is" "round" "+")
int4
Fiona is cold.
("Fiona" "is" "cold" "+")
int5
Charlie is not round.
Unknown
inv-rconc
[@1: Charlie is round.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "round" "-")
Charlie is rough.
Unknown
rconc
[@1: Charlie is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "rough" "+")
Charlie is not quiet.
Unknown
inv-rconc
[@3: Charlie is quiet.[CWA. Example of deepest failure = (rule7 <- rule2 <- rule6 <- FAIL)]]
("Charlie" "is" "quiet" "-")
Charlie is kind.
Unknown
rconc
[@1: Charlie is kind.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Charlie" "is" "kind" "+")
Charlie is not blue.
Unknown
inv-rconc
[@2: Charlie is blue.[CWA. Example of deepest failure = (rule2 <- rule6 <- FAIL)]]
("Charlie" "is" "blue" "-")
Gary is smart.
Unknown
random
[@0: Gary is smart.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "smart" "+")
@0: Charlie is not cold.[(triple1)] Fiona is smart.[(triple2)] Gary is cold.[(triple3)] Gary is kind.[(triple4)] Gary is round.[(triple5 OR ((triple3) -> rule6))] Harry is cold.[(triple6 OR ((triple10) -> rule5))] Harry is kind.[(triple7 OR ((triple10 ((((triple10) -> rule3)) -> rule7)) -> rule8) OR ((triple10 ((((triple9) -> rule2)) -> rule7)) -> rule8) OR ((triple10 ((((((triple6) -> rule6)) -> rule2)) -> rule7)) -> rule8) OR ((triple10 ((((((((triple10) -> rule5)) -> rule6)) -> rule2)) -> rule7)) -> rule8))] Harry is rough.[(triple8 OR ((triple6) -> rule1) OR ((((triple10) -> rule5)) -> rule1))] Harry is round.[(triple9 OR ((triple6) -> rule6) OR ((((triple10) -> rule5)) -> rule6) OR ((triple6 ((((triple10) -> rule3)) -> rule7)) -> rule4) OR ((((triple10) -> rule5) ((((triple10) -> rule3)) -> rule7)) -> rule4))] Harry is smart.[(triple10)] @1: Fiona is cold.[(((triple2) -> rule5))] Gary is blue.[(((triple5) -> rule2) OR ((((triple3) -> rule6)) -> rule2))] Gary is rough.[(((triple3) -> rule1))] Harry is blue.[(((triple10) -> rule3) OR ((triple9) -> rule2) OR ((((triple6) -> rule6)) -> rule2) OR ((((((triple10) -> rule5)) -> rule6)) -> rule2))] @2: Fiona is rough.[(((((triple2) -> rule5)) -> rule1))] Fiona is round.[(((((triple2) -> rule5)) -> rule6))] Gary is quiet.[(((((triple5) -> rule2)) -> rule7) OR ((((((triple3) -> rule6)) -> rule2)) -> rule7))] Harry is quiet.[(((((triple10) -> rule3)) -> rule7) OR ((((triple9) -> rule2)) -> rule7) OR ((((((triple6) -> rule6)) -> rule2)) -> rule7) OR ((((((((triple10) -> rule5)) -> rule6)) -> rule2)) -> rule7))] @3: Fiona is blue.[(((((((triple2) -> rule5)) -> rule6)) -> rule2))] @4: Fiona is quiet.[(((((((((triple2) -> rule5)) -> rule6)) -> rule2)) -> rule7))] @5: Fiona is kind.[(((triple2 ((((((((triple2) -> rule5)) -> rule6)) -> rule2)) -> rule7)) -> rule8))]
Charlie is not cold.
("Charlie" "is" "cold" "-")
triple1
Fiona is smart.
("Fiona" "is" "smart" "+")
triple2
Gary is cold.
("Gary" "is" "cold" "+")
triple3
Gary is kind.
("Gary" "is" "kind" "+")
triple4
Gary is round.
("Gary" "is" "round" "+")
triple5
((triple3) -> (rule6 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
triple6
((triple10) -> (rule5 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
triple7
((triple10 ((((triple10) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
((triple10 ((((triple9) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
((triple10 ((((((triple6) -> (rule6 % int4))) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is round.
("Harry" "is" "round" "+")
int4
((triple10 ((((((((triple10) -> (rule5 % int5))) -> (rule6 % int4))) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is round.
("Harry" "is" "round" "+")
int4
Harry is cold.
("Harry" "is" "cold" "+")
int5
Harry is rough.
("Harry" "is" "rough" "+")
triple8
((triple6) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
((((triple10) -> (rule5 % int2))) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
triple9
((triple6) -> (rule6 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
((((triple10) -> (rule5 % int2))) -> (rule6 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
((triple6 ((((triple10) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
((((triple10) -> (rule5 % int4)) ((((triple10) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is cold.
("Harry" "is" "cold" "+")
int4
Harry is smart.
("Harry" "is" "smart" "+")
triple10
Fiona is cold.
("Fiona" "is" "cold" "+")
((triple2) -> (rule5 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
((triple5) -> (rule2 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
((((triple3) -> (rule6 % int2))) -> (rule2 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
((triple3) -> (rule1 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
((triple10) -> (rule3 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
((triple9) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
((((triple6) -> (rule6 % int2))) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
((((((triple10) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Fiona is rough.
("Fiona" "is" "rough" "+")
((((triple2) -> (rule5 % int2))) -> (rule1 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
((((triple2) -> (rule5 % int2))) -> (rule6 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
((((triple5) -> (rule2 % int2))) -> (rule7 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
((((((triple3) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Harry is quiet.
("Harry" "is" "quiet" "+")
((((triple10) -> (rule3 % int2))) -> (rule7 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
((((triple9) -> (rule2 % int2))) -> (rule7 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
((((((triple6) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
((((((((triple10) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is cold.
("Harry" "is" "cold" "+")
int4
Fiona is blue.
("Fiona" "is" "blue" "+")
((((((triple2) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((((((((triple2) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
int3
Fiona is cold.
("Fiona" "is" "cold" "+")
int4
Fiona is kind.
("Fiona" "is" "kind" "+")
((triple2 ((((((((triple2) -> (rule5 % int5))) -> (rule6 % int4))) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
Fiona is round.
("Fiona" "is" "round" "+")
int4
Fiona is cold.
("Fiona" "is" "cold" "+")
int5