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