Anne is big. Anne is blue. Anne is round. Anne is white. Bob is big. Bob is blue. Bob is kind. Bob is round. Bob is smart. Bob is young. Erin is big. Gary is big. Gary is blue. Gary is smart. Gary is white. If something is big then it is smart. If something is smart then it is young. If Erin is kind and Erin is white then Erin is round. If Anne is round then Anne is kind. If something is blue and white then it is smart. If Gary is round and Gary is young then Gary is blue.
Anne is big.
("Anne" "is" "big" "+")
Anne is blue.
("Anne" "is" "blue" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is white.
("Anne" "is" "white" "+")
Bob is big.
("Bob" "is" "big" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is young.
("Bob" "is" "young" "+")
Erin is big.
("Erin" "is" "big" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is white.
("Gary" "is" "white" "+")
If something is big then it is smart.
((("something" "is" "big" "+")) -> ("something" "is" "smart" "+"))
If something is smart then it is young.
((("something" "is" "smart" "+")) -> ("something" "is" "young" "+"))
If Erin is kind and Erin is white then Erin is round.
((("Erin" "is" "kind" "+") ("Erin" "is" "white" "+")) -> ("Erin" "is" "round" "+"))
If Anne is round then Anne is kind.
((("Anne" "is" "round" "+")) -> ("Anne" "is" "kind" "+"))
If something is blue and white then it is smart.
((("something" "is" "blue" "+") ("something" "is" "white" "+")) -> ("something" "is" "smart" "+"))
If Gary is round and Gary is young then Gary is blue.
((("Gary" "is" "round" "+") ("Gary" "is" "young" "+")) -> ("Gary" "is" "blue" "+"))
Gary is big.
True
1
proof
[(triple12)]
("Gary" "is" "big" "+")
triple12
Gary is not big.
False
1
inv-proof
[(triple12)]
("Gary" "is" "big" "-")
triple12
Anne is kind.
True
2
proof
[(((triple3) -> rule4))]
("Anne" "is" "kind" "+")
((triple3) -> (rule4 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is not smart.
False
2
inv-proof
[(((triple1) -> rule1) OR ((triple2 triple4) -> rule5))]
("Anne" "is" "smart" "-")
((triple1) -> (rule1 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
((triple2 triple4) -> (rule5 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is young.
True
3
proof
[(((((triple1) -> rule1)) -> rule2) OR ((((triple2 triple4) -> rule5)) -> rule2))]
("Anne" "is" "young" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
((((triple2 triple4) -> (rule5 % int2))) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is not young.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule2) OR ((((triple2 triple4) -> rule5)) -> rule2))]
("Anne" "is" "young" "-")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
((((triple2 triple4) -> (rule5 % int2))) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Erin is not round.
Unknown
inv-rconc
[@1: Erin is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Erin" "is" "round" "-")
Erin is blue.
Unknown
random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "+")
Bob is not white.
Unknown
inv-random
[@0: Bob is white.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "white" "-")
Gary is round.
Unknown
random
[@0: Gary is round.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "round" "+")
Erin is not white.
Unknown
inv-random
[@0: Erin is white.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "white" "-")
Erin is kind.
Unknown
random
[@0: Erin is kind.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "kind" "+")
@0: Anne is big.[(triple1)] Anne is blue.[(triple2)] Anne is round.[(triple3)] Anne is white.[(triple4)] Bob is big.[(triple5)] Bob is blue.[(triple6)] Bob is kind.[(triple7)] Bob is round.[(triple8)] Bob is smart.[(triple9 OR ((triple5) -> rule1))] Bob is young.[(triple10 OR ((triple9) -> rule2) OR ((((triple5) -> rule1)) -> rule2))] Erin is big.[(triple11)] Gary is big.[(triple12)] Gary is blue.[(triple13)] Gary is smart.[(triple14 OR ((triple12) -> rule1) OR ((triple13 triple15) -> rule5))] Gary is white.[(triple15)] @1: Anne is kind.[(((triple3) -> rule4))] Anne is smart.[(((triple1) -> rule1) OR ((triple2 triple4) -> rule5))] Erin is smart.[(((triple11) -> rule1))] Gary is young.[(((triple14) -> rule2) OR ((((triple12) -> rule1)) -> rule2) OR ((((triple13 triple15) -> rule5)) -> rule2))] @2: Anne is young.[(((((triple1) -> rule1)) -> rule2) OR ((((triple2 triple4) -> rule5)) -> rule2))] Erin is young.[(((((triple11) -> rule1)) -> rule2))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is blue.
("Anne" "is" "blue" "+")
triple2
Anne is round.
("Anne" "is" "round" "+")
triple3
Anne is white.
("Anne" "is" "white" "+")
triple4
Bob is big.
("Bob" "is" "big" "+")
triple5
Bob is blue.
("Bob" "is" "blue" "+")
triple6
Bob is kind.
("Bob" "is" "kind" "+")
triple7
Bob is round.
("Bob" "is" "round" "+")
triple8
Bob is smart.
("Bob" "is" "smart" "+")
triple9
((triple5) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
triple10
((triple9) -> (rule2 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
((((triple5) -> (rule1 % int2))) -> (rule2 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
triple11
Gary is big.
("Gary" "is" "big" "+")
triple12
Gary is blue.
("Gary" "is" "blue" "+")
triple13
Gary is smart.
("Gary" "is" "smart" "+")
triple14
((triple12) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
((triple13 triple15) -> (rule5 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
triple15
Anne is kind.
("Anne" "is" "kind" "+")
((triple3) -> (rule4 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
((triple1) -> (rule1 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
((triple2 triple4) -> (rule5 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
((triple11) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
((triple14) -> (rule2 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
((((triple12) -> (rule1 % int2))) -> (rule2 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
((((triple13 triple15) -> (rule5 % int2))) -> (rule2 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
((((triple2 triple4) -> (rule5 % int2))) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
((((triple11) -> (rule1 % int2))) -> (rule2 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2