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