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