Anne is quiet. Bob is furry. Bob is quiet. Bob is red. Bob is white. Bob is young. Charlie is furry. Charlie is green. Charlie is quiet. Charlie is red. Charlie is young. Erin is green. If someone is green and red then they are smart. If Charlie is white and Charlie is furry then Charlie is quiet. If someone is furry and young then they are green.
Anne is quiet.
("Anne" "is" "quiet" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is white.
("Bob" "is" "white" "+")
Bob is young.
("Bob" "is" "young" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Erin is green.
("Erin" "is" "green" "+")
If someone is green and red then they are smart.
((("someone" "is" "green" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "smart" "+"))
If Charlie is white and Charlie is furry then Charlie is quiet.
((("Charlie" "is" "white" "+") ("Charlie" "is" "furry" "+")) -> ("Charlie" "is" "quiet" "+"))
If someone is furry and young then they are green.
((("someone" "is" "furry" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "green" "+"))
Charlie is red.
True
1
proof
[(triple10)]
("Charlie" "is" "red" "+")
triple10
Erin is not green.
False
1
inv-proof
[(triple12)]
("Erin" "is" "green" "-")
triple12
Charlie is smart.
True
3
proof
[(((triple8 triple10) -> rule1) OR ((((triple7 triple11) -> rule3) triple10) -> rule1))]
("Charlie" "is" "smart" "+")
((triple8 triple10) -> (rule1 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
((((triple7 triple11) -> (rule3 % int2)) triple10) -> (rule1 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is not smart.
False
3
inv-proof
[(((triple8 triple10) -> rule1) OR ((((triple7 triple11) -> rule3) triple10) -> rule1))]
("Charlie" "is" "smart" "-")
((triple8 triple10) -> (rule1 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
((((triple7 triple11) -> (rule3 % int2)) triple10) -> (rule1 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Bob is smart.
True
5
proof
[(((((triple2 triple6) -> rule3) triple4) -> rule1))]
("Bob" "is" "smart" "+")
((((triple2 triple6) -> (rule3 % int2)) triple4) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is not smart.
False
5
inv-proof
[(((((triple2 triple6) -> rule3) triple4) -> rule1))]
("Bob" "is" "smart" "-")
((((triple2 triple6) -> (rule3 % int2)) triple4) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Erin is not smart.
Unknown
inv-rconc
[@1: Erin is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "smart" "-")
Anne is green.
Unknown
rconc
[@1: Anne is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "green" "+")
Anne is not smart.
Unknown
inv-rconc
[@1: Anne is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "smart" "-")
Anne is red.
Unknown
random
[@0: Anne is red.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "red" "+")
Erin is not white.
Unknown
inv-random
[@0: Erin is white.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "white" "-")
Erin is furry.
Unknown
random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "+")
@0: Anne is quiet.[(triple1)] Bob is furry.[(triple2)] Bob is quiet.[(triple3)] Bob is red.[(triple4)] Bob is white.[(triple5)] Bob is young.[(triple6)] Charlie is furry.[(triple7)] Charlie is green.[(triple8 OR ((triple7 triple11) -> rule3))] Charlie is quiet.[(triple9)] Charlie is red.[(triple10)] Charlie is young.[(triple11)] Erin is green.[(triple12)] @1: Bob is green.[(((triple2 triple6) -> rule3))] Charlie is smart.[(((triple8 triple10) -> rule1) OR ((((triple7 triple11) -> rule3) triple10) -> rule1))] @2: Bob is smart.[(((((triple2 triple6) -> rule3) triple4) -> rule1))]
Anne is quiet.
("Anne" "is" "quiet" "+")
triple1
Bob is furry.
("Bob" "is" "furry" "+")
triple2
Bob is quiet.
("Bob" "is" "quiet" "+")
triple3
Bob is red.
("Bob" "is" "red" "+")
triple4
Bob is white.
("Bob" "is" "white" "+")
triple5
Bob is young.
("Bob" "is" "young" "+")
triple6
Charlie is furry.
("Charlie" "is" "furry" "+")
triple7
Charlie is green.
("Charlie" "is" "green" "+")
triple8
((triple7 triple11) -> (rule3 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple9
Charlie is red.
("Charlie" "is" "red" "+")
triple10
Charlie is young.
("Charlie" "is" "young" "+")
triple11
Erin is green.
("Erin" "is" "green" "+")
triple12
Bob is green.
("Bob" "is" "green" "+")
((triple2 triple6) -> (rule3 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple8 triple10) -> (rule1 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
((((triple7 triple11) -> (rule3 % int2)) triple10) -> (rule1 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
((((triple2 triple6) -> (rule3 % int2)) triple4) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2