Anne is nice. Anne is red. Anne is not smart. Bob is blue. Bob is nice. Bob is quiet. Charlie is big. Charlie is smart. Gary is blue. Gary is not quiet. Gary is red. Gary is smart. All big people are round. If Charlie is red then Charlie is not blue. All red people are big.
Anne is nice.
("Anne" "is" "nice" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is not smart.
("Anne" "is" "smart" "-")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is not quiet.
("Gary" "is" "quiet" "-")
Gary is red.
("Gary" "is" "red" "+")
Gary is smart.
("Gary" "is" "smart" "+")
All big people are round.
((("someone" "is" "big" "+")) -> ("someone" "is" "round" "+"))
If Charlie is red then Charlie is not blue.
((("Charlie" "is" "red" "+")) -> ("Charlie" "is" "blue" "-"))
All red people are big.
((("someone" "is" "red" "+")) -> ("someone" "is" "big" "+"))
Gary is smart.
True
1
proof
[(triple12)]
("Gary" "is" "smart" "+")
triple12
Gary is quiet.
False
1
inv-proof
[(triple10)]
("Gary" "is" "quiet" "+")
triple10
Gary is big.
True
2
proof
[(((triple11) -> rule3))]
("Gary" "is" "big" "+")
((triple11) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Charlie is not round.
False
2
inv-proof
[(((triple7) -> rule1))]
("Charlie" "is" "round" "-")
((triple7) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Gary is round.
True
3
proof
[(((((triple11) -> rule3)) -> rule1))]
("Gary" "is" "round" "+")
((((triple11) -> (rule3 % int2))) -> (rule1 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Anne is not round.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule1))]
("Anne" "is" "round" "-")
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Bob is not big.
Unknown
inv-rconc
[@1: Bob is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "big" "-")
Bob is round.
Unknown
rconc
[@2: Bob is round.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("Bob" "is" "round" "+")
Charlie is not quiet.
Unknown
inv-random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "-")
Bob is smart.
Unknown
random
[@0: Bob is smart.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "smart" "+")
Anne is not quiet.
Unknown
inv-random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "-")
Charlie is red.
Unknown
random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "+")
@0: Anne is nice.[(triple1)] Anne is not smart.[(triple3)] Anne is red.[(triple2)] Bob is blue.[(triple4)] Bob is nice.[(triple5)] Bob is quiet.[(triple6)] Charlie is big.[(triple7)] Charlie is smart.[(triple8)] Gary is blue.[(triple9)] Gary is not quiet.[(triple10)] Gary is red.[(triple11)] Gary is smart.[(triple12)] @1: Anne is big.[(((triple2) -> rule3))] Charlie is round.[(((triple7) -> rule1))] Gary is big.[(((triple11) -> rule3))] @2: Anne is round.[(((((triple2) -> rule3)) -> rule1))] Gary is round.[(((((triple11) -> rule3)) -> rule1))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Anne is not smart.
("Anne" "is" "smart" "-")
triple3
Anne is red.
("Anne" "is" "red" "+")
triple2
Bob is blue.
("Bob" "is" "blue" "+")
triple4
Bob is nice.
("Bob" "is" "nice" "+")
triple5
Bob is quiet.
("Bob" "is" "quiet" "+")
triple6
Charlie is big.
("Charlie" "is" "big" "+")
triple7
Charlie is smart.
("Charlie" "is" "smart" "+")
triple8
Gary is blue.
("Gary" "is" "blue" "+")
triple9
Gary is not quiet.
("Gary" "is" "quiet" "-")
triple10
Gary is red.
("Gary" "is" "red" "+")
triple11
Gary is smart.
("Gary" "is" "smart" "+")
triple12
Anne is big.
("Anne" "is" "big" "+")
((triple2) -> (rule3 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
((triple7) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
((triple11) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
((((triple11) -> (rule3 % int2))) -> (rule1 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2