Bob is red. Charlie is round. Charlie is not white. Charlie is young. Dave is white. Dave is not young. Gary is big. If Bob is white then Bob is smart. Smart people are blue. If Gary is big then Gary is red. If someone is red then they are white. Big, white people are smart. All round, red people are big. If someone is white and blue then they are young.
Bob is red.
("Bob" "is" "red" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is not white.
("Charlie" "is" "white" "-")
Charlie is young.
("Charlie" "is" "young" "+")
Dave is white.
("Dave" "is" "white" "+")
Dave is not young.
("Dave" "is" "young" "-")
Gary is big.
("Gary" "is" "big" "+")
If Bob is white then Bob is smart.
((("Bob" "is" "white" "+")) -> ("Bob" "is" "smart" "+"))
Smart people are blue.
((("someone" "is" "smart" "+")) -> ("someone" "is" "blue" "+"))
If Gary is big then Gary is red.
((("Gary" "is" "big" "+")) -> ("Gary" "is" "red" "+"))
If someone is red then they are white.
((("someone" "is" "red" "+")) -> ("someone" "is" "white" "+"))
Big, white people are smart.
((("someone" "is" "big" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "smart" "+"))
All round, red people are big.
((("someone" "is" "round" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "big" "+"))
If someone is white and blue then they are young.
((("someone" "is" "white" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "young" "+"))
Charlie is not white.
True
1
proof
[(triple3)]
("Charlie" "is" "white" "-")
triple3
Dave is young.
False
1
inv-proof
[(triple6)]
("Dave" "is" "young" "+")
triple6
Bob is white.
True
2
proof
[(((triple1) -> rule4))]
("Bob" "is" "white" "+")
((triple1) -> (rule4 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is not white.
False
2
inv-proof
[(((triple1) -> rule4))]
("Bob" "is" "white" "-")
((triple1) -> (rule4 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is smart.
True
3
proof
[(((((triple1) -> rule4)) -> rule1))]
("Bob" "is" "smart" "+")
((((triple1) -> (rule4 % int2))) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Gary is not white.
False
3
inv-proof
[(((((triple7) -> rule3)) -> rule4))]
("Gary" "is" "white" "-")
((((triple7) -> (rule3 % int2))) -> (rule4 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is smart.
True
5
proof
[(((triple7 ((((triple7) -> rule3)) -> rule4)) -> rule5))]
("Gary" "is" "smart" "+")
((triple7 ((((triple7) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Bob is not blue.
False
4
inv-proof
[(((((((triple1) -> rule4)) -> rule1)) -> rule2))]
("Bob" "is" "blue" "-")
((((((triple1) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is young.
True
7
proof
[(((((triple1) -> rule4) ((((((triple1) -> rule4)) -> rule1)) -> rule2)) -> rule7))]
("Bob" "is" "young" "+")
((((triple1) -> (rule4 % int4)) ((((((triple1) -> (rule4 % int4))) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
int4
Bob is not young.
False
7
inv-proof
[(((((triple1) -> rule4) ((((((triple1) -> rule4)) -> rule1)) -> rule2)) -> rule7))]
("Bob" "is" "young" "-")
((((triple1) -> (rule4 % int4)) ((((((triple1) -> (rule4 % int4))) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
int4
Gary is young.
True
10
proof
[(((((((triple7) -> rule3)) -> rule4) ((((triple7 ((((triple7) -> rule3)) -> rule4)) -> rule5)) -> rule2)) -> rule7))]
("Gary" "is" "young" "+")
((((((triple7) -> (rule3 % int5))) -> (rule4 % int4)) ((((triple7 ((((triple7) -> (rule3 % int5))) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is white.
("Gary" "is" "white" "+")
int4
Gary is red.
("Gary" "is" "red" "+")
int5
Gary is not young.
False
10
inv-proof
[(((((((triple7) -> rule3)) -> rule4) ((((triple7 ((((triple7) -> rule3)) -> rule4)) -> rule5)) -> rule2)) -> rule7))]
("Gary" "is" "young" "-")
((((((triple7) -> (rule3 % int5))) -> (rule4 % int4)) ((((triple7 ((((triple7) -> (rule3 % int5))) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is white.
("Gary" "is" "white" "+")
int4
Gary is red.
("Gary" "is" "red" "+")
int5
Dave is not big.
Unknown
inv-rconc
[@1: Dave is big.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Dave" "is" "big" "-")
Bob is big.
Unknown
rconc
[@1: Bob is big.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Bob" "is" "big" "+")
Charlie is not big.
Unknown
inv-rconc
[@1: Charlie is big.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "big" "-")
Charlie is smart.
Unknown
rconc
[@1: Charlie is smart.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Charlie" "is" "smart" "+")
Dave is not blue.
Unknown
inv-rconc
[@3: Dave is blue.[CWA. Example of deepest failure = (rule2 <- rule5 <- rule6 <- FAIL)]]
("Dave" "is" "blue" "-")
Charlie is blue.
Unknown
rconc
[@2: Charlie is blue.[CWA. Example of deepest failure = (rule2 <- rule5 <- FAIL)]]
("Charlie" "is" "blue" "+")
Charlie is not red.
Unknown
inv-random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "-")
Bob is round.
Unknown
random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "+")
Dave is not round.
Unknown
inv-random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "-")
Gary is round.
Unknown
random
[@0: Gary is round.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "round" "+")
@0: Bob is red.[(triple1)] Charlie is not white.[(triple3)] Charlie is round.[(triple2)] Charlie is young.[(triple4)] Dave is not young.[(triple6)] Dave is white.[(triple5)] Gary is big.[(triple7)] @1: Bob is white.[(((triple1) -> rule4))] Gary is red.[(((triple7) -> rule3))] @2: Bob is smart.[(((((triple1) -> rule4)) -> rule1))] Gary is white.[(((((triple7) -> rule3)) -> rule4))] @3: Bob is blue.[(((((((triple1) -> rule4)) -> rule1)) -> rule2))] Gary is smart.[(((triple7 ((((triple7) -> rule3)) -> rule4)) -> rule5))] @4: Bob is young.[(((((triple1) -> rule4) ((((((triple1) -> rule4)) -> rule1)) -> rule2)) -> rule7))] Gary is blue.[(((((triple7 ((((triple7) -> rule3)) -> rule4)) -> rule5)) -> rule2))] @5: Gary is young.[(((((((triple7) -> rule3)) -> rule4) ((((triple7 ((((triple7) -> rule3)) -> rule4)) -> rule5)) -> rule2)) -> rule7))]
Bob is red.
("Bob" "is" "red" "+")
triple1
Charlie is not white.
("Charlie" "is" "white" "-")
triple3
Charlie is round.
("Charlie" "is" "round" "+")
triple2
Charlie is young.
("Charlie" "is" "young" "+")
triple4
Dave is not young.
("Dave" "is" "young" "-")
triple6
Dave is white.
("Dave" "is" "white" "+")
triple5
Gary is big.
("Gary" "is" "big" "+")
triple7
Bob is white.
("Bob" "is" "white" "+")
((triple1) -> (rule4 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
((triple7) -> (rule3 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
((((triple1) -> (rule4 % int2))) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
((((triple7) -> (rule3 % int2))) -> (rule4 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
((((((triple1) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Gary is smart.
("Gary" "is" "smart" "+")
((triple7 ((((triple7) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Bob is young.
("Bob" "is" "young" "+")
((((triple1) -> (rule4 % int4)) ((((((triple1) -> (rule4 % int4))) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
int4
Gary is blue.
("Gary" "is" "blue" "+")
((((triple7 ((((triple7) -> (rule3 % int4))) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is red.
("Gary" "is" "red" "+")
int4
Gary is young.
("Gary" "is" "young" "+")
((((((triple7) -> (rule3 % int5))) -> (rule4 % int4)) ((((triple7 ((((triple7) -> (rule3 % int5))) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is white.
("Gary" "is" "white" "+")
int4
Gary is red.
("Gary" "is" "red" "+")
int5