Charlie is rough. Dave is furry. Erin is blue. Erin is cold. Erin is smart. Harry is big. Harry is blue. Harry is furry. Harry is kind. Harry is smart. All kind people are blue. If someone is smart and furry then they are kind. Big, blue people are kind. If someone is big and smart then they are rough. All furry people are smart. If someone is blue then they are rough.
Charlie is rough.
("Charlie" "is" "rough" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is smart.
("Harry" "is" "smart" "+")
All kind people are blue.
((("someone" "is" "kind" "+")) -> ("someone" "is" "blue" "+"))
If someone is smart and furry then they are kind.
((("someone" "is" "smart" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "kind" "+"))
Big, blue people are kind.
((("someone" "is" "big" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "kind" "+"))
If someone is big and smart then they are rough.
((("someone" "is" "big" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "rough" "+"))
All furry people are smart.
((("someone" "is" "furry" "+")) -> ("someone" "is" "smart" "+"))
If someone is blue then they are rough.
((("someone" "is" "blue" "+")) -> ("someone" "is" "rough" "+"))
Harry is kind.
True
1
proof
[(triple9 OR ((triple10 triple8) -> rule2) OR ((triple6 triple7) -> rule3) OR ((((triple8) -> rule5) triple8) -> rule2))]
("Harry" "is" "kind" "+")
triple9
((triple10 triple8) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((triple6 triple7) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((((triple8) -> (rule5 % int2)) triple8) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is not blue.
False
1
inv-proof
[(triple7 OR ((triple9) -> rule1) OR ((((triple10 triple8) -> rule2)) -> rule1) OR ((((((triple8) -> rule5) triple8) -> rule2)) -> rule1))]
("Harry" "is" "blue" "-")
triple7
((triple9) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
((((triple10 triple8) -> (rule2 % int2))) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
((((((triple8) -> (rule5 % int3)) triple8) -> (rule2 % int2))) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
Dave is smart.
True
2
proof
[(((triple2) -> rule5))]
("Dave" "is" "smart" "+")
((triple2) -> (rule5 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Erin is not rough.
False
2
inv-proof
[(((triple3) -> rule6))]
("Erin" "is" "rough" "-")
((triple3) -> (rule6 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Dave is kind.
True
4
proof
[(((((triple2) -> rule5) triple2) -> rule2))]
("Dave" "is" "kind" "+")
((((triple2) -> (rule5 % int2)) triple2) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is not kind.
False
4
inv-proof
[(((((triple2) -> rule5) triple2) -> rule2))]
("Dave" "is" "kind" "-")
((((triple2) -> (rule5 % int2)) triple2) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is blue.
True
5
proof
[(((((((triple2) -> rule5) triple2) -> rule2)) -> rule1))]
("Dave" "is" "blue" "+")
((((((triple2) -> (rule5 % int3)) triple2) -> (rule2 % int2))) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is not blue.
False
5
inv-proof
[(((((((triple2) -> rule5) triple2) -> rule2)) -> rule1))]
("Dave" "is" "blue" "-")
((((((triple2) -> (rule5 % int3)) triple2) -> (rule2 % int2))) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Charlie is not blue.
Unknown
inv-rconc
[@2: Charlie is blue.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Charlie" "is" "blue" "-")
Erin is kind.
Unknown
rconc
[@1: Erin is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "kind" "+")
Charlie is not smart.
Unknown
inv-rconc
[@1: Charlie is smart.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Charlie" "is" "smart" "-")
Charlie is kind.
Unknown
rconc
[@1: Charlie is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "kind" "+")
Dave is not big.
Unknown
inv-random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "-")
Dave is cold.
Unknown
random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "+")
Charlie is not cold.
Unknown
inv-random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "-")
Charlie is furry.
Unknown
random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "+")
@0: Charlie is rough.[(triple1)] Dave is furry.[(triple2)] Erin is blue.[(triple3)] Erin is cold.[(triple4)] Erin is smart.[(triple5)] Harry is big.[(triple6)] Harry is blue.[(triple7 OR ((triple9) -> rule1) OR ((((triple10 triple8) -> rule2)) -> rule1) OR ((((((triple8) -> rule5) triple8) -> rule2)) -> rule1))] Harry is furry.[(triple8)] Harry is kind.[(triple9 OR ((triple10 triple8) -> rule2) OR ((triple6 triple7) -> rule3) OR ((((triple8) -> rule5) triple8) -> rule2))] Harry is smart.[(triple10 OR ((triple8) -> rule5))] @1: Dave is smart.[(((triple2) -> rule5))] Erin is rough.[(((triple3) -> rule6))] Harry is rough.[(((triple7) -> rule6) OR ((triple6 triple10) -> rule4) OR ((((triple9) -> rule1)) -> rule6) OR ((triple6 ((triple8) -> rule5)) -> rule4) OR ((((((triple10 triple8) -> rule2)) -> rule1)) -> rule6) OR ((((((((triple8) -> rule5) triple8) -> rule2)) -> rule1)) -> rule6))] @2: Dave is kind.[(((((triple2) -> rule5) triple2) -> rule2))] @3: Dave is blue.[(((((((triple2) -> rule5) triple2) -> rule2)) -> rule1))] @4: Dave is rough.[(((((((((triple2) -> rule5) triple2) -> rule2)) -> rule1)) -> rule6))]
Charlie is rough.
("Charlie" "is" "rough" "+")
triple1
Dave is furry.
("Dave" "is" "furry" "+")
triple2
Erin is blue.
("Erin" "is" "blue" "+")
triple3
Erin is cold.
("Erin" "is" "cold" "+")
triple4
Erin is smart.
("Erin" "is" "smart" "+")
triple5
Harry is big.
("Harry" "is" "big" "+")
triple6
Harry is blue.
("Harry" "is" "blue" "+")
triple7
((triple9) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
((((triple10 triple8) -> (rule2 % int2))) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
((((((triple8) -> (rule5 % int3)) triple8) -> (rule2 % int2))) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
Harry is furry.
("Harry" "is" "furry" "+")
triple8
Harry is kind.
("Harry" "is" "kind" "+")
triple9
((triple10 triple8) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((triple6 triple7) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((((triple8) -> (rule5 % int2)) triple8) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
triple10
((triple8) -> (rule5 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
((triple2) -> (rule5 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
((triple3) -> (rule6 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
((triple7) -> (rule6 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
((triple6 triple10) -> (rule4 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
((((triple9) -> (rule1 % int2))) -> (rule6 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
((triple6 ((triple8) -> (rule5 % int2))) -> (rule4 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
((((((triple10 triple8) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
((((((((triple8) -> (rule5 % int4)) triple8) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Harry is smart.
("Harry" "is" "smart" "+")
int4
Dave is kind.
("Dave" "is" "kind" "+")
((((triple2) -> (rule5 % int2)) triple2) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
((((((triple2) -> (rule5 % int3)) triple2) -> (rule2 % int2))) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
((((((((triple2) -> (rule5 % int4)) triple2) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Dave is smart.
("Dave" "is" "smart" "+")
int4