Bob is kind. Bob is round. Bob is young. Charlie is round. Charlie is young. Dave is kind. Dave is quiet. Dave is white. Dave is young. Harry is big. Harry is cold. Harry is young. All white people are young. If someone is quiet then they are white. All round, white people are quiet. If someone is round then they are white. Quiet people are cold. If Bob is young then Bob is white.
Bob is kind.
("Bob" "is" "kind" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is young.
("Bob" "is" "young" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is white.
("Dave" "is" "white" "+")
Dave is young.
("Dave" "is" "young" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is young.
("Harry" "is" "young" "+")
All white people are young.
((("someone" "is" "white" "+")) -> ("someone" "is" "young" "+"))
If someone is quiet then they are white.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "white" "+"))
All round, white people are quiet.
((("someone" "is" "round" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "quiet" "+"))
If someone is round then they are white.
((("someone" "is" "round" "+")) -> ("someone" "is" "white" "+"))
Quiet people are cold.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "cold" "+"))
If Bob is young then Bob is white.
((("Bob" "is" "young" "+")) -> ("Bob" "is" "white" "+"))
Harry is cold.
True
1
proof
[(triple11)]
("Harry" "is" "cold" "+")
triple11
Dave is not young.
False
1
inv-proof
[(triple9 OR ((triple8) -> rule1) OR ((((triple7) -> rule2)) -> rule1))]
("Dave" "is" "young" "-")
triple9
((triple8) -> (rule1 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
((((triple7) -> (rule2 % int2))) -> (rule1 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Charlie is white.
True
2
proof
[(((triple4) -> rule4))]
("Charlie" "is" "white" "+")
((triple4) -> (rule4 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is not white.
False
2
inv-proof
[(((triple4) -> rule4))]
("Charlie" "is" "white" "-")
((triple4) -> (rule4 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Bob is quiet.
True
4
proof
[(((triple2 ((triple2) -> rule4)) -> rule3) OR ((triple2 ((triple3) -> rule6)) -> rule3))]
("Bob" "is" "quiet" "+")
((triple2 ((triple2) -> (rule4 % int2))) -> (rule3 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
((triple2 ((triple3) -> (rule6 % int2))) -> (rule3 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is not quiet.
False
4
inv-proof
[(((triple2 ((triple2) -> rule4)) -> rule3) OR ((triple2 ((triple3) -> rule6)) -> rule3))]
("Bob" "is" "quiet" "-")
((triple2 ((triple2) -> (rule4 % int2))) -> (rule3 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
((triple2 ((triple3) -> (rule6 % int2))) -> (rule3 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is cold.
True
5
proof
[(((((triple2 ((triple2) -> rule4)) -> rule3)) -> rule5) OR ((((triple2 ((triple3) -> rule6)) -> rule3)) -> rule5))]
("Bob" "is" "cold" "+")
((((triple2 ((triple2) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
((((triple2 ((triple3) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is not cold.
False
5
inv-proof
[(((((triple2 ((triple2) -> rule4)) -> rule3)) -> rule5) OR ((((triple2 ((triple3) -> rule6)) -> rule3)) -> rule5))]
("Bob" "is" "cold" "-")
((((triple2 ((triple2) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
((((triple2 ((triple3) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Harry is not white.
Unknown
inv-rconc
[@2: Harry is white.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("Harry" "is" "white" "-")
Harry is quiet.
Unknown
rconc
[@1: Harry is quiet.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "quiet" "+")
Dave is not round.
Unknown
inv-random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "-")
Bob is big.
Unknown
random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "+")
Charlie is not kind.
Unknown
inv-random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "-")
Dave is big.
Unknown
random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "+")
Harry is not round.
Unknown
inv-random
[@0: Harry is round.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "round" "-")
Charlie is big.
Unknown
random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "+")
@0: Bob is kind.[(triple1)] Bob is round.[(triple2)] Bob is young.[(triple3 OR ((((triple2) -> rule4)) -> rule1))] Charlie is round.[(triple4)] Charlie is young.[(triple5 OR ((((triple4) -> rule4)) -> rule1))] Dave is kind.[(triple6)] Dave is quiet.[(triple7)] Dave is white.[(triple8 OR ((triple7) -> rule2))] Dave is young.[(triple9 OR ((triple8) -> rule1) OR ((((triple7) -> rule2)) -> rule1))] Harry is big.[(triple10)] Harry is cold.[(triple11)] Harry is young.[(triple12)] @1: Bob is white.[(((triple2) -> rule4) OR ((triple3) -> rule6))] Charlie is white.[(((triple4) -> rule4))] Dave is cold.[(((triple7) -> rule5))] @2: Bob is quiet.[(((triple2 ((triple2) -> rule4)) -> rule3) OR ((triple2 ((triple3) -> rule6)) -> rule3))] Charlie is quiet.[(((triple4 ((triple4) -> rule4)) -> rule3))] @3: Bob is cold.[(((((triple2 ((triple2) -> rule4)) -> rule3)) -> rule5) OR ((((triple2 ((triple3) -> rule6)) -> rule3)) -> rule5))] Charlie is cold.[(((((triple4 ((triple4) -> rule4)) -> rule3)) -> rule5))]
Bob is kind.
("Bob" "is" "kind" "+")
triple1
Bob is round.
("Bob" "is" "round" "+")
triple2
Bob is young.
("Bob" "is" "young" "+")
triple3
((((triple2) -> (rule4 % int2))) -> (rule1 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
triple4
Charlie is young.
("Charlie" "is" "young" "+")
triple5
((((triple4) -> (rule4 % int2))) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
triple6
Dave is quiet.
("Dave" "is" "quiet" "+")
triple7
Dave is white.
("Dave" "is" "white" "+")
triple8
((triple7) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
triple9
((triple8) -> (rule1 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
((((triple7) -> (rule2 % int2))) -> (rule1 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
triple10
Harry is cold.
("Harry" "is" "cold" "+")
triple11
Harry is young.
("Harry" "is" "young" "+")
triple12
Bob is white.
("Bob" "is" "white" "+")
((triple2) -> (rule4 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
((triple3) -> (rule6 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
((triple4) -> (rule4 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
((triple7) -> (rule5 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
((triple2 ((triple2) -> (rule4 % int2))) -> (rule3 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
((triple2 ((triple3) -> (rule6 % int2))) -> (rule3 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple4 ((triple4) -> (rule4 % int2))) -> (rule3 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
((((triple2 ((triple2) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
((((triple2 ((triple3) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Charlie is cold.
("Charlie" "is" "cold" "+")
((((triple4 ((triple4) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3