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