Anne is furry. Anne is green. Anne is quiet. Anne is red. Anne is smart. Bob is quiet. Bob is smart. Dave is furry. Dave is quiet. Erin is green. If someone is big then they are smart. Red people are green. Red people are green. Red people are green. All green people are rough. If someone is smart and red then they are rough. Furry people are big. If someone is red and not rough then they are quiet.
Anne is furry.
("Anne" "is" "furry" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Erin is green.
("Erin" "is" "green" "+")
If someone is big then they are smart.
((("someone" "is" "big" "+")) -> ("someone" "is" "smart" "+"))
Red people are green.
((("someone" "is" "red" "+")) -> ("someone" "is" "green" "+"))
Red people are green.
((("someone" "is" "red" "+")) -> ("someone" "is" "green" "+"))
Red people are green.
((("someone" "is" "red" "+")) -> ("someone" "is" "green" "+"))
All green people are rough.
((("someone" "is" "green" "+")) -> ("someone" "is" "rough" "+"))
If someone is smart and red then they are rough.
((("someone" "is" "smart" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "rough" "+"))
Furry people are big.
((("someone" "is" "furry" "+")) -> ("someone" "is" "big" "+"))
If someone is red and not rough then they are quiet.
((("someone" "is" "red" "+") ("someone" "is" "rough" "~")) -> ("someone" "is" "quiet" "+"))
Erin is green.
True
1
proof
[(triple10)]
("Erin" "is" "green" "+")
triple10
Bob is not smart.
False
1
inv-proof
[(triple7)]
("Bob" "is" "smart" "-")
triple7
Anne is rough.
True
2
proof
[(((triple2) -> rule5) OR ((triple5 triple4) -> rule6) OR ((((triple4) -> rule2)) -> rule5) OR ((((triple4) -> rule3)) -> rule5) OR ((((triple4) -> rule4)) -> rule5) OR ((((((triple1) -> rule7)) -> rule1) triple4) -> rule6))]
("Anne" "is" "rough" "+")
((triple2) -> (rule5 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
((triple5 triple4) -> (rule6 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
((((triple4) -> (rule2 % int2))) -> (rule5 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
((((triple4) -> (rule3 % int2))) -> (rule5 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
((((triple4) -> (rule4 % int2))) -> (rule5 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
((((((triple1) -> (rule7 % int3))) -> (rule1 % int2)) triple4) -> (rule6 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Anne is not big.
False
2
inv-proof
[(((triple1) -> rule7))]
("Anne" "is" "big" "-")
((triple1) -> (rule7 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Dave is smart.
True
3
proof
[(((((triple8) -> rule7)) -> rule1))]
("Dave" "is" "smart" "+")
((((triple8) -> (rule7 % int2))) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is not smart.
False
3
inv-proof
[(((((triple8) -> rule7)) -> rule1))]
("Dave" "is" "smart" "-")
((((triple8) -> (rule7 % int2))) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Bob is not big.
Unknown
inv-rconc
[@1: Bob is big.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Bob" "is" "big" "-")
Erin is smart.
Unknown
rconc
[@2: Erin is smart.[CWA. Example of deepest failure = (rule1 <- rule7 <- FAIL)]]
("Erin" "is" "smart" "+")
Dave is not green.
Unknown
inv-rconc
[@1: Dave is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "green" "-")
Bob is furry.
Unknown
random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "+")
Bob is not red.
Unknown
inv-random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "-")
Erin is furry.
Unknown
random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "+")
@0: Anne is furry.[(triple1)] Anne is green.[(triple2 OR ((triple4) -> rule2) OR ((triple4) -> rule3) OR ((triple4) -> rule4))] Anne is quiet.[(triple3)] Anne is red.[(triple4)] Anne is smart.[(triple5 OR ((((triple1) -> rule7)) -> rule1))] Bob is quiet.[(triple6)] Bob is smart.[(triple7)] Dave is furry.[(triple8)] Dave is quiet.[(triple9)] Erin is green.[(triple10)] @1: Anne is big.[(((triple1) -> rule7))] Anne is rough.[(((triple2) -> rule5) OR ((triple5 triple4) -> rule6) OR ((((triple4) -> rule2)) -> rule5) OR ((((triple4) -> rule3)) -> rule5) OR ((((triple4) -> rule4)) -> rule5) OR ((((((triple1) -> rule7)) -> rule1) triple4) -> rule6))] Dave is big.[(((triple8) -> rule7))] Erin is rough.[(((triple10) -> rule5))] @2: Dave is smart.[(((((triple8) -> rule7)) -> rule1))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Anne is green.
("Anne" "is" "green" "+")
triple2
((triple4) -> (rule2 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
((triple4) -> (rule3 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
((triple4) -> (rule4 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
triple3
Anne is red.
("Anne" "is" "red" "+")
triple4
Anne is smart.
("Anne" "is" "smart" "+")
triple5
((((triple1) -> (rule7 % int2))) -> (rule1 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
triple6
Bob is smart.
("Bob" "is" "smart" "+")
triple7
Dave is furry.
("Dave" "is" "furry" "+")
triple8
Dave is quiet.
("Dave" "is" "quiet" "+")
triple9
Erin is green.
("Erin" "is" "green" "+")
triple10
Anne is big.
("Anne" "is" "big" "+")
((triple1) -> (rule7 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
((triple2) -> (rule5 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
((triple5 triple4) -> (rule6 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
((((triple4) -> (rule2 % int2))) -> (rule5 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
((((triple4) -> (rule3 % int2))) -> (rule5 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
((((triple4) -> (rule4 % int2))) -> (rule5 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
((((((triple1) -> (rule7 % int3))) -> (rule1 % int2)) triple4) -> (rule6 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Dave is big.
("Dave" "is" "big" "+")
((triple8) -> (rule7 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
((triple10) -> (rule5 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
((((triple8) -> (rule7 % int2))) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2