Bob is big. Charlie is furry. Charlie is green. Dave is big. Dave is blue. Dave is furry. Dave is white. Erin is big. Erin is blue. Erin is white. If something is furry then it is nice. If something is rough then it is nice. All white things are nice. Nice things are white. Furry, blue things are rough. All furry things are white. If something is white then it is green. All nice things are furry.
Bob is big.
("Bob" "is" "big" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is white.
("Dave" "is" "white" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is white.
("Erin" "is" "white" "+")
If something is furry then it is nice.
((("something" "is" "furry" "+")) -> ("something" "is" "nice" "+"))
If something is rough then it is nice.
((("something" "is" "rough" "+")) -> ("something" "is" "nice" "+"))
All white things are nice.
((("something" "is" "white" "+")) -> ("something" "is" "nice" "+"))
Nice things are white.
((("something" "is" "nice" "+")) -> ("something" "is" "white" "+"))
Furry, blue things are rough.
((("something" "is" "furry" "+") ("something" "is" "blue" "+")) -> ("something" "is" "rough" "+"))
All furry things are white.
((("something" "is" "furry" "+")) -> ("something" "is" "white" "+"))
If something is white then it is green.
((("something" "is" "white" "+")) -> ("something" "is" "green" "+"))
All nice things are furry.
((("something" "is" "nice" "+")) -> ("something" "is" "furry" "+"))
Dave is white.
True
1
proof
[(triple7 OR ((triple6) -> rule6) OR ((((triple6) -> rule1)) -> rule4) OR ((((((triple6 triple5) -> rule5)) -> rule2)) -> rule4))]
("Dave" "is" "white" "+")
triple7
((triple6) -> (rule6 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
((((triple6) -> (rule1 % int2))) -> (rule4 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
((((((triple6 triple5) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Charlie is not green.
False
1
inv-proof
[(triple3 OR ((((triple2) -> rule6)) -> rule7) OR ((((((triple2) -> rule1)) -> rule4)) -> rule7))]
("Charlie" "is" "green" "-")
triple3
((((triple2) -> (rule6 % int2))) -> (rule7 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
((((((triple2) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Erin is green.
True
2
proof
[(((triple10) -> rule7))]
("Erin" "is" "green" "+")
((triple10) -> (rule7 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Dave is not rough.
False
3
inv-proof
[(((triple6 triple5) -> rule5) OR ((((((triple7) -> rule3)) -> rule8) triple5) -> rule5))]
("Dave" "is" "rough" "-")
((triple6 triple5) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
((((((triple7) -> (rule3 % int3))) -> (rule8 % int2)) triple5) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Bob is not white.
Unknown
inv-rconc
[@6: Bob is white.[CWA. Example of deepest failure = (rule4 <- rule3 <- rule6 <- rule8 <- rule2 <- rule5 <- FAIL)]]
("Bob" "is" "white" "-")
Bob is rough.
Unknown
rconc
[@1: Bob is rough.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Bob" "is" "rough" "+")
Charlie is not big.
Unknown
inv-random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "-")
Charlie is blue.
Unknown
random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "+")
@0: Bob is big.[(triple1)] Charlie is furry.[(triple2)] Charlie is green.[(triple3 OR ((((triple2) -> rule6)) -> rule7) OR ((((((triple2) -> rule1)) -> rule4)) -> rule7))] Dave is big.[(triple4)] Dave is blue.[(triple5)] Dave is furry.[(triple6 OR ((((triple7) -> rule3)) -> rule8))] Dave is white.[(triple7 OR ((triple6) -> rule6) OR ((((triple6) -> rule1)) -> rule4) OR ((((((triple6 triple5) -> rule5)) -> rule2)) -> rule4))] Erin is big.[(triple8)] Erin is blue.[(triple9)] Erin is white.[(triple10)] @1: Charlie is nice.[(((triple2) -> rule1) OR ((((triple2) -> rule6)) -> rule3))] Charlie is white.[(((triple2) -> rule6) OR ((((triple2) -> rule1)) -> rule4))] Dave is green.[(((triple7) -> rule7) OR ((((triple6) -> rule6)) -> rule7) OR ((((((triple6) -> rule1)) -> rule4)) -> rule7) OR ((((((((triple6 triple5) -> rule5)) -> rule2)) -> rule4)) -> rule7))] Dave is nice.[(((triple6) -> rule1) OR ((triple7) -> rule3) OR ((((triple6) -> rule6)) -> rule3) OR ((((triple6 triple5) -> rule5)) -> rule2))] Dave is rough.[(((triple6 triple5) -> rule5) OR ((((((triple7) -> rule3)) -> rule8) triple5) -> rule5))] Erin is green.[(((triple10) -> rule7))] Erin is nice.[(((triple10) -> rule3))] @2: Erin is furry.[(((((triple10) -> rule3)) -> rule8))] @3: Erin is rough.[(((((((triple10) -> rule3)) -> rule8) triple9) -> rule5))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple2
Charlie is green.
("Charlie" "is" "green" "+")
triple3
((((triple2) -> (rule6 % int2))) -> (rule7 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
((((((triple2) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Dave is big.
("Dave" "is" "big" "+")
triple4
Dave is blue.
("Dave" "is" "blue" "+")
triple5
Dave is furry.
("Dave" "is" "furry" "+")
triple6
((((triple7) -> (rule3 % int2))) -> (rule8 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
triple7
((triple6) -> (rule6 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
((((triple6) -> (rule1 % int2))) -> (rule4 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
((((((triple6 triple5) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Erin is big.
("Erin" "is" "big" "+")
triple8
Erin is blue.
("Erin" "is" "blue" "+")
triple9
Erin is white.
("Erin" "is" "white" "+")
triple10
Charlie is nice.
("Charlie" "is" "nice" "+")
((triple2) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
((((triple2) -> (rule6 % int2))) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
((triple2) -> (rule6 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
((((triple2) -> (rule1 % int2))) -> (rule4 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
((triple7) -> (rule7 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
((((triple6) -> (rule6 % int2))) -> (rule7 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
((((((triple6) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
((((((((triple6 triple5) -> (rule5 % int4))) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
int4
Dave is nice.
("Dave" "is" "nice" "+")
((triple6) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((triple7) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((((triple6) -> (rule6 % int2))) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
((((triple6 triple5) -> (rule5 % int2))) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
((triple6 triple5) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
((((((triple7) -> (rule3 % int3))) -> (rule8 % int2)) triple5) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Erin is green.
("Erin" "is" "green" "+")
((triple10) -> (rule7 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
((triple10) -> (rule3 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
((((triple10) -> (rule3 % int2))) -> (rule8 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
((((((triple10) -> (rule3 % int3))) -> (rule8 % int2)) triple9) -> (rule5 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3