Anne is nice. Anne is white. Bob is furry. Charlie is kind. Charlie is rough. Charlie is smart. Dave is white. All white, nice people are rough. All white people are blue. All kind, white people are smart. Furry people are nice. If someone is rough then they are blue. All white people are kind. If Dave is white and Dave is smart then Dave is furry.
Anne is nice.
("Anne" "is" "nice" "+")
Anne is white.
("Anne" "is" "white" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Dave is white.
("Dave" "is" "white" "+")
All white, nice people are rough.
((("someone" "is" "white" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "rough" "+"))
All white people are blue.
((("someone" "is" "white" "+")) -> ("someone" "is" "blue" "+"))
All kind, white people are smart.
((("someone" "is" "kind" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "smart" "+"))
Furry people are nice.
((("someone" "is" "furry" "+")) -> ("someone" "is" "nice" "+"))
If someone is rough then they are blue.
((("someone" "is" "rough" "+")) -> ("someone" "is" "blue" "+"))
All white people are kind.
((("someone" "is" "white" "+")) -> ("someone" "is" "kind" "+"))
If Dave is white and Dave is smart then Dave is furry.
((("Dave" "is" "white" "+") ("Dave" "is" "smart" "+")) -> ("Dave" "is" "furry" "+"))
Bob is furry.
True
1
proof
[(triple3)]
("Bob" "is" "furry" "+")
triple3
Charlie is not rough.
False
1
inv-proof
[(triple5)]
("Charlie" "is" "rough" "-")
triple5
Charlie is blue.
True
2
proof
[(((triple5) -> rule5))]
("Charlie" "is" "blue" "+")
((triple5) -> (rule5 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Anne is not blue.
False
2
inv-proof
[(((triple2) -> rule2) OR ((((triple2 triple1) -> rule1)) -> rule5))]
("Anne" "is" "blue" "-")
((triple2) -> (rule2 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
((((triple2 triple1) -> (rule1 % int2))) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Dave is smart.
True
4
proof
[(((((triple7) -> rule6) triple7) -> rule3))]
("Dave" "is" "smart" "+")
((((triple7) -> (rule6 % int2)) triple7) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Anne is not smart.
False
4
inv-proof
[(((((triple2) -> rule6) triple2) -> rule3))]
("Anne" "is" "smart" "-")
((((triple2) -> (rule6 % int2)) triple2) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Dave is furry.
True
6
proof
[(((triple7 ((((triple7) -> rule6) triple7) -> rule3)) -> rule7))]
("Dave" "is" "furry" "+")
((triple7 ((((triple7) -> (rule6 % int3)) triple7) -> (rule3 % int2))) -> (rule7 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Dave is not furry.
False
6
inv-proof
[(((triple7 ((((triple7) -> rule6) triple7) -> rule3)) -> rule7))]
("Dave" "is" "furry" "-")
((triple7 ((((triple7) -> (rule6 % int3)) triple7) -> (rule3 % int2))) -> (rule7 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Dave is nice.
True
7
proof
[(((((triple7 ((((triple7) -> rule6) triple7) -> rule3)) -> rule7)) -> rule4))]
("Dave" "is" "nice" "+")
((((triple7 ((((triple7) -> (rule6 % int4)) triple7) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is kind.
("Dave" "is" "kind" "+")
int4
Dave is not nice.
False
7
inv-proof
[(((((triple7 ((((triple7) -> rule6) triple7) -> rule3)) -> rule7)) -> rule4))]
("Dave" "is" "nice" "-")
((((triple7 ((((triple7) -> (rule6 % int4)) triple7) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is kind.
("Dave" "is" "kind" "+")
int4
Dave is rough.
True
9
proof
[(((triple7 ((((triple7 ((((triple7) -> rule6) triple7) -> rule3)) -> rule7)) -> rule4)) -> rule1))]
("Dave" "is" "rough" "+")
((triple7 ((((triple7 ((((triple7) -> (rule6 % int5)) triple7) -> (rule3 % int4))) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is smart.
("Dave" "is" "smart" "+")
int4
Dave is kind.
("Dave" "is" "kind" "+")
int5
Dave is not rough.
False
9
inv-proof
[(((triple7 ((((triple7 ((((triple7) -> rule6) triple7) -> rule3)) -> rule7)) -> rule4)) -> rule1))]
("Dave" "is" "rough" "-")
((triple7 ((((triple7 ((((triple7) -> (rule6 % int5)) triple7) -> (rule3 % int4))) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is smart.
("Dave" "is" "smart" "+")
int4
Dave is kind.
("Dave" "is" "kind" "+")
int5
Charlie is not nice.
Unknown
inv-rconc
[@1: Charlie is nice.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Charlie" "is" "nice" "-")
Bob is kind.
Unknown
rconc
[@1: Bob is kind.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Bob" "is" "kind" "+")
Bob is not rough.
Unknown
inv-rconc
[@1: Bob is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "rough" "-")
Bob is smart.
Unknown
rconc
[@1: Bob is smart.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "smart" "+")
Bob is not blue.
Unknown
inv-rconc
[@2: Bob is blue.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("Bob" "is" "blue" "-")
Charlie is white.
Unknown
random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "+")
Anne is not furry.
Unknown
inv-random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "-")
Bob is white.
Unknown
random
[@0: Bob is white.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "white" "+")
@0: Anne is nice.[(triple1)] Anne is white.[(triple2)] Bob is furry.[(triple3)] Charlie is kind.[(triple4)] Charlie is rough.[(triple5)] Charlie is smart.[(triple6)] Dave is white.[(triple7)] @1: Anne is blue.[(((triple2) -> rule2) OR ((((triple2 triple1) -> rule1)) -> rule5))] Anne is kind.[(((triple2) -> rule6))] Anne is rough.[(((triple2 triple1) -> rule1))] Bob is nice.[(((triple3) -> rule4))] Charlie is blue.[(((triple5) -> rule5))] Dave is blue.[(((triple7) -> rule2) OR ((((triple7 ((((triple7 ((((triple7) -> rule6) triple7) -> rule3)) -> rule7)) -> rule4)) -> rule1)) -> rule5))] Dave is kind.[(((triple7) -> rule6))] @2: Anne is smart.[(((((triple2) -> rule6) triple2) -> rule3))] Dave is smart.[(((((triple7) -> rule6) triple7) -> rule3))] @3: Dave is furry.[(((triple7 ((((triple7) -> rule6) triple7) -> rule3)) -> rule7))] @4: Dave is nice.[(((((triple7 ((((triple7) -> rule6) triple7) -> rule3)) -> rule7)) -> rule4))] @5: Dave is rough.[(((triple7 ((((triple7 ((((triple7) -> rule6) triple7) -> rule3)) -> rule7)) -> rule4)) -> rule1))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Anne is white.
("Anne" "is" "white" "+")
triple2
Bob is furry.
("Bob" "is" "furry" "+")
triple3
Charlie is kind.
("Charlie" "is" "kind" "+")
triple4
Charlie is rough.
("Charlie" "is" "rough" "+")
triple5
Charlie is smart.
("Charlie" "is" "smart" "+")
triple6
Dave is white.
("Dave" "is" "white" "+")
triple7
Anne is blue.
("Anne" "is" "blue" "+")
((triple2) -> (rule2 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
((((triple2 triple1) -> (rule1 % int2))) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
((triple2) -> (rule6 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
((triple2 triple1) -> (rule1 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
((triple3) -> (rule4 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
((triple5) -> (rule5 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
((triple7) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((((triple7 ((((triple7 ((((triple7) -> (rule6 % int6)) triple7) -> (rule3 % int5))) -> (rule7 % int4))) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is furry.
("Dave" "is" "furry" "+")
int4
Dave is smart.
("Dave" "is" "smart" "+")
int5
Dave is kind.
("Dave" "is" "kind" "+")
int6
Dave is kind.
("Dave" "is" "kind" "+")
((triple7) -> (rule6 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
((((triple2) -> (rule6 % int2)) triple2) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
((((triple7) -> (rule6 % int2)) triple7) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
((triple7 ((((triple7) -> (rule6 % int3)) triple7) -> (rule3 % int2))) -> (rule7 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
((((triple7 ((((triple7) -> (rule6 % int4)) triple7) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is kind.
("Dave" "is" "kind" "+")
int4
Dave is rough.
("Dave" "is" "rough" "+")
((triple7 ((((triple7 ((((triple7) -> (rule6 % int5)) triple7) -> (rule3 % int4))) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is smart.
("Dave" "is" "smart" "+")
int4
Dave is kind.
("Dave" "is" "kind" "+")
int5