Anne is smart. Anne is white. Bob is furry. Bob is round. Bob is white. Bob is young. Charlie is green. Charlie is smart. Charlie is white. Charlie is young. Erin is furry. Erin is green. Erin is round. Erin is white. Erin is young. If Bob is smart and Bob is furry then Bob is quiet. If Charlie is round and Charlie is young then Charlie is smart. If Bob is green and Bob is white then Bob is round. If someone is green and young then they are quiet. Smart people are white. All green people are smart. If Erin is white and Erin is young then Erin is furry. Round people are smart.
Anne is smart.
("Anne" "is" "smart" "+")
Anne is white.
("Anne" "is" "white" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is white.
("Bob" "is" "white" "+")
Bob is young.
("Bob" "is" "young" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is white.
("Erin" "is" "white" "+")
Erin is young.
("Erin" "is" "young" "+")
If Bob is smart and Bob is furry then Bob is quiet.
((("Bob" "is" "smart" "+") ("Bob" "is" "furry" "+")) -> ("Bob" "is" "quiet" "+"))
If Charlie is round and Charlie is young then Charlie is smart.
((("Charlie" "is" "round" "+") ("Charlie" "is" "young" "+")) -> ("Charlie" "is" "smart" "+"))
If Bob is green and Bob is white then Bob is round.
((("Bob" "is" "green" "+") ("Bob" "is" "white" "+")) -> ("Bob" "is" "round" "+"))
If someone is green and young then they are quiet.
((("someone" "is" "green" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "quiet" "+"))
Smart people are white.
((("someone" "is" "smart" "+")) -> ("someone" "is" "white" "+"))
All green people are smart.
((("someone" "is" "green" "+")) -> ("someone" "is" "smart" "+"))
If Erin is white and Erin is young then Erin is furry.
((("Erin" "is" "white" "+") ("Erin" "is" "young" "+")) -> ("Erin" "is" "furry" "+"))
Round people are smart.
((("someone" "is" "round" "+")) -> ("someone" "is" "smart" "+"))
Bob is furry.
True
1
proof
[(triple3)]
("Bob" "is" "furry" "+")
triple3
Bob is not young.
False
1
inv-proof
[(triple6)]
("Bob" "is" "young" "-")
triple6
Charlie is quiet.
True
3
proof
[(((triple7 triple10) -> rule4))]
("Charlie" "is" "quiet" "+")
((triple7 triple10) -> (rule4 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is not quiet.
False
3
inv-proof
[(((triple7 triple10) -> rule4))]
("Charlie" "is" "quiet" "-")
((triple7 triple10) -> (rule4 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Anne is not quiet.
Unknown
inv-rconc
[@1: Anne is quiet.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Anne" "is" "quiet" "-")
Bob is green.
Unknown
random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "+")
Anne is not green.
Unknown
inv-random
[@0: Anne is green.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "green" "-")
Anne is furry.
Unknown
random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "+")
@0: Anne is smart.[(triple1)] Anne is white.[(triple2 OR ((triple1) -> rule5))] Bob is furry.[(triple3)] Bob is round.[(triple4)] Bob is white.[(triple5 OR ((((triple4) -> rule8)) -> rule5))] Bob is young.[(triple6)] Charlie is green.[(triple7)] Charlie is smart.[(triple8 OR ((triple7) -> rule6))] Charlie is white.[(triple9 OR ((triple8) -> rule5) OR ((((triple7) -> rule6)) -> rule5))] Charlie is young.[(triple10)] Erin is furry.[(triple11 OR ((triple14 triple15) -> rule7) OR ((((((triple12) -> rule6)) -> rule5) triple15) -> rule7) OR ((((((triple13) -> rule8)) -> rule5) triple15) -> rule7))] Erin is green.[(triple12)] Erin is round.[(triple13)] Erin is white.[(triple14 OR ((((triple12) -> rule6)) -> rule5) OR ((((triple13) -> rule8)) -> rule5))] Erin is young.[(triple15)] @1: Bob is smart.[(((triple4) -> rule8))] Charlie is quiet.[(((triple7 triple10) -> rule4))] Erin is quiet.[(((triple12 triple15) -> rule4))] Erin is smart.[(((triple12) -> rule6) OR ((triple13) -> rule8))] @2: Bob is quiet.[(((((triple4) -> rule8) triple3) -> rule1))]
Anne is smart.
("Anne" "is" "smart" "+")
triple1
Anne is white.
("Anne" "is" "white" "+")
triple2
((triple1) -> (rule5 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
triple3
Bob is round.
("Bob" "is" "round" "+")
triple4
Bob is white.
("Bob" "is" "white" "+")
triple5
((((triple4) -> (rule8 % int2))) -> (rule5 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
triple6
Charlie is green.
("Charlie" "is" "green" "+")
triple7
Charlie is smart.
("Charlie" "is" "smart" "+")
triple8
((triple7) -> (rule6 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
triple9
((triple8) -> (rule5 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
((((triple7) -> (rule6 % int2))) -> (rule5 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
triple10
Erin is furry.
("Erin" "is" "furry" "+")
triple11
((triple14 triple15) -> (rule7 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
((((((triple12) -> (rule6 % int3))) -> (rule5 % int2)) triple15) -> (rule7 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
((((((triple13) -> (rule8 % int3))) -> (rule5 % int2)) triple15) -> (rule7 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is green.
("Erin" "is" "green" "+")
triple12
Erin is round.
("Erin" "is" "round" "+")
triple13
Erin is white.
("Erin" "is" "white" "+")
triple14
((((triple12) -> (rule6 % int2))) -> (rule5 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
((((triple13) -> (rule8 % int2))) -> (rule5 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
triple15
Bob is smart.
("Bob" "is" "smart" "+")
((triple4) -> (rule8 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple7 triple10) -> (rule4 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
((triple12 triple15) -> (rule4 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
((triple12) -> (rule6 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((triple13) -> (rule8 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
((((triple4) -> (rule8 % int2)) triple3) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2