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