Anne is blue. Anne is round. Anne is young. Bob is round. Bob is young. Erin is big. Harry is furry. If something is furry then it is blue. Round things are white. If Erin is blue and Erin is young then Erin is white. If Bob is rough then Bob is big. If something is blue then it is rough. If Anne is round then Anne is furry. If something is young and white then it is furry.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is young.
("Anne" "is" "young" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is young.
("Bob" "is" "young" "+")
Erin is big.
("Erin" "is" "big" "+")
Harry is furry.
("Harry" "is" "furry" "+")
If something is furry then it is blue.
((("something" "is" "furry" "+")) -> ("something" "is" "blue" "+"))
Round things are white.
((("something" "is" "round" "+")) -> ("something" "is" "white" "+"))
If Erin is blue and Erin is young then Erin is white.
((("Erin" "is" "blue" "+") ("Erin" "is" "young" "+")) -> ("Erin" "is" "white" "+"))
If Bob is rough then Bob is big.
((("Bob" "is" "rough" "+")) -> ("Bob" "is" "big" "+"))
If something is blue then it is rough.
((("something" "is" "blue" "+")) -> ("something" "is" "rough" "+"))
If Anne is round then Anne is furry.
((("Anne" "is" "round" "+")) -> ("Anne" "is" "furry" "+"))
If something is young and white then it is furry.
((("something" "is" "young" "+") ("something" "is" "white" "+")) -> ("something" "is" "furry" "+"))
Anne is young.
True
1
proof
[(triple3)]
("Anne" "is" "young" "+")
triple3
Anne is not blue.
False
1
inv-proof
[(triple1 OR ((((triple2) -> rule6)) -> rule1) OR ((((triple3 ((triple2) -> rule2)) -> rule7)) -> rule1))]
("Anne" "is" "blue" "-")
triple1
((((triple2) -> (rule6 % int2))) -> (rule1 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
((((triple3 ((triple2) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Bob is white.
True
2
proof
[(((triple4) -> rule2))]
("Bob" "is" "white" "+")
((triple4) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Anne is not rough.
False
2
inv-proof
[(((triple1) -> rule5) OR ((((((triple2) -> rule6)) -> rule1)) -> rule5) OR ((((((triple3 ((triple2) -> rule2)) -> rule7)) -> rule1)) -> rule5))]
("Anne" "is" "rough" "-")
((triple1) -> (rule5 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
((((((triple2) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
((((((triple3 ((triple2) -> (rule2 % int4))) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is white.
("Anne" "is" "white" "+")
int4
Bob is furry.
True
4
proof
[(((triple5 ((triple4) -> rule2)) -> rule7))]
("Bob" "is" "furry" "+")
((triple5 ((triple4) -> (rule2 % int2))) -> (rule7 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is not furry.
False
4
inv-proof
[(((triple5 ((triple4) -> rule2)) -> rule7))]
("Bob" "is" "furry" "-")
((triple5 ((triple4) -> (rule2 % int2))) -> (rule7 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is blue.
True
5
proof
[(((((triple5 ((triple4) -> rule2)) -> rule7)) -> rule1))]
("Bob" "is" "blue" "+")
((((triple5 ((triple4) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is not blue.
False
5
inv-proof
[(((((triple5 ((triple4) -> rule2)) -> rule7)) -> rule1))]
("Bob" "is" "blue" "-")
((((triple5 ((triple4) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is rough.
True
6
proof
[(((((((triple5 ((triple4) -> rule2)) -> rule7)) -> rule1)) -> rule5))]
("Bob" "is" "rough" "+")
((((((triple5 ((triple4) -> (rule2 % int4))) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
int4
Bob is not rough.
False
6
inv-proof
[(((((((triple5 ((triple4) -> rule2)) -> rule7)) -> rule1)) -> rule5))]
("Bob" "is" "rough" "-")
((((((triple5 ((triple4) -> (rule2 % int4))) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
int4
Bob is big.
True
7
proof
[(((((((((triple5 ((triple4) -> rule2)) -> rule7)) -> rule1)) -> rule5)) -> rule4))]
("Bob" "is" "big" "+")
((((((((triple5 ((triple4) -> (rule2 % int5))) -> (rule7 % int4))) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Bob is furry.
("Bob" "is" "furry" "+")
int4
Bob is white.
("Bob" "is" "white" "+")
int5
Bob is not big.
False
7
inv-proof
[(((((((((triple5 ((triple4) -> rule2)) -> rule7)) -> rule1)) -> rule5)) -> rule4))]
("Bob" "is" "big" "-")
((((((((triple5 ((triple4) -> (rule2 % int5))) -> (rule7 % int4))) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Bob is furry.
("Bob" "is" "furry" "+")
int4
Bob is white.
("Bob" "is" "white" "+")
int5
Erin is not white.
Unknown
inv-rconc
[@1: Erin is white.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "white" "-")
Erin is rough.
Unknown
rconc
[@3: Erin is rough.[CWA. Example of deepest failure = (rule5 <- rule1 <- rule7 <- FAIL)]]
("Erin" "is" "rough" "+")
Erin is not furry.
Unknown
inv-rconc
[@1: Erin is furry.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Erin" "is" "furry" "-")
Harry is white.
Unknown
rconc
[@1: Harry is white.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "white" "+")
Erin is not blue.
Unknown
inv-rconc
[@2: Erin is blue.[CWA. Example of deepest failure = (rule1 <- rule7 <- FAIL)]]
("Erin" "is" "blue" "-")
Harry is round.
Unknown
random
[@0: Harry is round.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "round" "+")
Erin is not round.
Unknown
inv-random
[@0: Erin is round.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "round" "-")
Anne is big.
Unknown
random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "+")
Harry is not big.
Unknown
inv-random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "-")
Harry is young.
Unknown
random
[@0: Harry is young.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "young" "+")
@0: Anne is blue.[(triple1 OR ((((triple2) -> rule6)) -> rule1) OR ((((triple3 ((triple2) -> rule2)) -> rule7)) -> rule1))] Anne is round.[(triple2)] Anne is young.[(triple3)] Bob is round.[(triple4)] Bob is young.[(triple5)] Erin is big.[(triple6)] Harry is furry.[(triple7)] @1: Anne is furry.[(((triple2) -> rule6) OR ((triple3 ((triple2) -> rule2)) -> rule7))] Anne is rough.[(((triple1) -> rule5) OR ((((((triple2) -> rule6)) -> rule1)) -> rule5) OR ((((((triple3 ((triple2) -> rule2)) -> rule7)) -> rule1)) -> rule5))] Anne is white.[(((triple2) -> rule2))] Bob is white.[(((triple4) -> rule2))] Harry is blue.[(((triple7) -> rule1))] @2: Bob is furry.[(((triple5 ((triple4) -> rule2)) -> rule7))] Harry is rough.[(((((triple7) -> rule1)) -> rule5))] @3: Bob is blue.[(((((triple5 ((triple4) -> rule2)) -> rule7)) -> rule1))] @4: Bob is rough.[(((((((triple5 ((triple4) -> rule2)) -> rule7)) -> rule1)) -> rule5))] @5: Bob is big.[(((((((((triple5 ((triple4) -> rule2)) -> rule7)) -> rule1)) -> rule5)) -> rule4))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
((((triple2) -> (rule6 % int2))) -> (rule1 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
((((triple3 ((triple2) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Anne is round.
("Anne" "is" "round" "+")
triple2
Anne is young.
("Anne" "is" "young" "+")
triple3
Bob is round.
("Bob" "is" "round" "+")
triple4
Bob is young.
("Bob" "is" "young" "+")
triple5
Erin is big.
("Erin" "is" "big" "+")
triple6
Harry is furry.
("Harry" "is" "furry" "+")
triple7
Anne is furry.
("Anne" "is" "furry" "+")
((triple2) -> (rule6 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
((triple3 ((triple2) -> (rule2 % int2))) -> (rule7 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
((triple1) -> (rule5 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
((((((triple2) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
((((((triple3 ((triple2) -> (rule2 % int4))) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is white.
("Anne" "is" "white" "+")
int4
Anne is white.
("Anne" "is" "white" "+")
((triple2) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
((triple4) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
((triple7) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
((triple5 ((triple4) -> (rule2 % int2))) -> (rule7 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
((((triple7) -> (rule1 % int2))) -> (rule5 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
((((triple5 ((triple4) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is rough.
("Bob" "is" "rough" "+")
((((((triple5 ((triple4) -> (rule2 % int4))) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
int4
Bob is big.
("Bob" "is" "big" "+")
((((((((triple5 ((triple4) -> (rule2 % int5))) -> (rule7 % int4))) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Bob is furry.
("Bob" "is" "furry" "+")
int4
Bob is white.
("Bob" "is" "white" "+")
int5