Anne is big. Anne is not nice. Anne is red. Anne is young. Dave is big. Dave is blue. Dave is not nice. Dave is red. Dave is rough. Dave is round. Dave is young. Gary is blue. Gary is nice. Gary is red. Gary is rough. If Gary is not nice then Gary is blue. If someone is big and nice then they are not rough. All red people are blue. All rough, red people are blue. If someone is blue and not big then they are round. If someone is nice and not rough then they are red. If someone is young and big then they are red. If someone is round and not nice then they are red.
Anne is big.
("Anne" "is" "big" "+")
Anne is not nice.
("Anne" "is" "nice" "-")
Anne is red.
("Anne" "is" "red" "+")
Anne is young.
("Anne" "is" "young" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is not nice.
("Dave" "is" "nice" "-")
Dave is red.
("Dave" "is" "red" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is young.
("Dave" "is" "young" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is rough.
("Gary" "is" "rough" "+")
If Gary is not nice then Gary is blue.
((("Gary" "is" "nice" "~")) -> ("Gary" "is" "blue" "+"))
If someone is big and nice then they are not rough.
((("someone" "is" "big" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "rough" "-"))
All red people are blue.
((("someone" "is" "red" "+")) -> ("someone" "is" "blue" "+"))
All rough, red people are blue.
((("someone" "is" "rough" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "blue" "+"))
If someone is blue and not big then they are round.
((("someone" "is" "blue" "+") ("someone" "is" "big" "~")) -> ("someone" "is" "round" "+"))
If someone is nice and not rough then they are red.
((("someone" "is" "nice" "+") ("someone" "is" "rough" "~")) -> ("someone" "is" "red" "+"))
If someone is young and big then they are red.
((("someone" "is" "young" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "red" "+"))
If someone is round and not nice then they are red.
((("someone" "is" "round" "+") ("someone" "is" "nice" "~")) -> ("someone" "is" "red" "+"))
Dave is big.
True
1
proof
[(triple5)]
("Dave" "is" "big" "+")
triple5
Dave is not rough.
False
1
inv-proof
[(triple9)]
("Dave" "is" "rough" "-")
triple9
Anne is blue.
True
2
proof
[(((triple3) -> rule3) OR ((((triple4 triple1) -> rule7)) -> rule3))]
("Anne" "is" "blue" "+")
((triple3) -> (rule3 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
((((triple4 triple1) -> (rule7 % int2))) -> (rule3 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is not blue.
False
2
inv-proof
[(((triple3) -> rule3) OR ((((triple4 triple1) -> rule7)) -> rule3))]
("Anne" "is" "blue" "-")
((triple3) -> (rule3 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
((((triple4 triple1) -> (rule7 % int2))) -> (rule3 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Gary is not round.
Unknown
inv-rconc
[@1: Gary is round.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Gary" "is" "round" "-")
Anne is round.
Unknown
rconc
[@1: Anne is round.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Anne" "is" "round" "+")
Anne is not rough.
Unknown
inv-random
[@0: Anne is rough.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "rough" "-")
Gary is big.
Unknown
random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "+")
@0: Anne is big.[(triple1)] Anne is not nice.[(triple2)] Anne is red.[(triple3 OR ((triple4 triple1) -> rule7))] Anne is young.[(triple4)] Dave is big.[(triple5)] Dave is blue.[(triple6 OR ((triple8) -> rule3) OR ((triple9 triple8) -> rule4) OR ((((triple10 triple7) -> rule8)) -> rule3) OR ((((triple11 triple5) -> rule7)) -> rule3) OR ((triple9 ((triple10 triple7) -> rule8)) -> rule4) OR ((triple9 ((triple11 triple5) -> rule7)) -> rule4))] Dave is not nice.[(triple7)] Dave is red.[(triple8 OR ((triple10 triple7) -> rule8) OR ((triple11 triple5) -> rule7))] Dave is rough.[(triple9)] Dave is round.[(triple10)] Dave is young.[(triple11)] Gary is blue.[(triple12 OR ((triple14) -> rule3) OR ((triple15 triple14) -> rule4))] Gary is nice.[(triple13)] Gary is red.[(triple14)] Gary is rough.[(triple15)] @1: Anne is blue.[(((triple3) -> rule3) OR ((((triple4 triple1) -> rule7)) -> rule3))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is not nice.
("Anne" "is" "nice" "-")
triple2
Anne is red.
("Anne" "is" "red" "+")
triple3
((triple4 triple1) -> (rule7 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
triple4
Dave is big.
("Dave" "is" "big" "+")
triple5
Dave is blue.
("Dave" "is" "blue" "+")
triple6
((triple8) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((triple9 triple8) -> (rule4 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((((triple10 triple7) -> (rule8 % int2))) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
((((triple11 triple5) -> (rule7 % int2))) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
((triple9 ((triple10 triple7) -> (rule8 % int2))) -> (rule4 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
((triple9 ((triple11 triple5) -> (rule7 % int2))) -> (rule4 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is not nice.
("Dave" "is" "nice" "-")
triple7
Dave is red.
("Dave" "is" "red" "+")
triple8
((triple10 triple7) -> (rule8 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
((triple11 triple5) -> (rule7 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
triple9
Dave is round.
("Dave" "is" "round" "+")
triple10
Dave is young.
("Dave" "is" "young" "+")
triple11
Gary is blue.
("Gary" "is" "blue" "+")
triple12
((triple14) -> (rule3 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
((triple15 triple14) -> (rule4 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
triple13
Gary is red.
("Gary" "is" "red" "+")
triple14
Gary is rough.
("Gary" "is" "rough" "+")
triple15
Anne is blue.
("Anne" "is" "blue" "+")
((triple3) -> (rule3 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
((((triple4 triple1) -> (rule7 % int2))) -> (rule3 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2