Bob is cold. Bob is red. Bob is rough. Bob is round. Bob is not smart. Erin is cold. Erin is round. Erin is smart. Harry is not big. Harry is kind. Harry is rough. Harry is round. All big things are not red. All smart, rough things are cold. If something is round and not kind then it is cold. If Erin is round and Erin is cold then Erin is big. If something is big and not smart then it is round. Kind things are round.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is not smart.
("Bob" "is" "smart" "-")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Harry is not big.
("Harry" "is" "big" "-")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is round.
("Harry" "is" "round" "+")
All big things are not red.
((("something" "is" "big" "+")) -> ("something" "is" "red" "-"))
All smart, rough things are cold.
((("something" "is" "smart" "+") ("something" "is" "rough" "+")) -> ("something" "is" "cold" "+"))
If something is round and not kind then it is cold.
((("something" "is" "round" "+") ("something" "is" "kind" "~")) -> ("something" "is" "cold" "+"))
If Erin is round and Erin is cold then Erin is big.
((("Erin" "is" "round" "+") ("Erin" "is" "cold" "+")) -> ("Erin" "is" "big" "+"))
If something is big and not smart then it is round.
((("something" "is" "big" "+") ("something" "is" "smart" "~")) -> ("something" "is" "round" "+"))
Kind things are round.
((("something" "is" "kind" "+")) -> ("something" "is" "round" "+"))
Bob is round.
True
1
proof
[(triple4)]
("Bob" "is" "round" "+")
triple4
Bob is not cold.
False
1
inv-proof
[(triple1)]
("Bob" "is" "cold" "-")
triple1
Erin is big.
True
3
proof
[(((triple7 triple6) -> rule4))]
("Erin" "is" "big" "+")
((triple7 triple6) -> (rule4 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is not big.
False
3
inv-proof
[(((triple7 triple6) -> rule4))]
("Erin" "is" "big" "-")
((triple7 triple6) -> (rule4 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is not red.
True
4
proof
[(((((triple7 triple6) -> rule4)) -> rule1))]
("Erin" "is" "red" "-")
((((triple7 triple6) -> (rule4 % int2))) -> (rule1 % int1))
Erin is not red.
("Erin" "is" "red" "-")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is red.
False
4
inv-proof
[(((((triple7 triple6) -> rule4)) -> rule1))]
("Erin" "is" "red" "+")
((((triple7 triple6) -> (rule4 % int2))) -> (rule1 % int1))
Erin is not red.
("Erin" "is" "red" "-")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Harry is not cold.
Unknown
inv-rconc
[@1: Harry is cold.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "cold" "-")
Erin is rough.
Unknown
random
[@0: Erin is rough.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "rough" "+")
Harry is not smart.
Unknown
inv-random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "-")
Bob is kind.
Unknown
random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "+")
Harry is not red.
Unknown
inv-random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "-")
Bob is big.
Unknown
random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "+")
@0: Bob is cold.[(triple1)] Bob is not smart.[(triple5)] Bob is red.[(triple2)] Bob is rough.[(triple3)] Bob is round.[(triple4)] Erin is cold.[(triple6)] Erin is round.[(triple7)] Erin is smart.[(triple8)] Harry is kind.[(triple10)] Harry is not big.[(triple9)] Harry is rough.[(triple11)] Harry is round.[(triple12 OR ((triple10) -> rule6))] @1: Erin is big.[(((triple7 triple6) -> rule4))] @2: Erin is not red.[(((((triple7 triple6) -> rule4)) -> rule1))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Bob is not smart.
("Bob" "is" "smart" "-")
triple5
Bob is red.
("Bob" "is" "red" "+")
triple2
Bob is rough.
("Bob" "is" "rough" "+")
triple3
Bob is round.
("Bob" "is" "round" "+")
triple4
Erin is cold.
("Erin" "is" "cold" "+")
triple6
Erin is round.
("Erin" "is" "round" "+")
triple7
Erin is smart.
("Erin" "is" "smart" "+")
triple8
Harry is kind.
("Harry" "is" "kind" "+")
triple10
Harry is not big.
("Harry" "is" "big" "-")
triple9
Harry is rough.
("Harry" "is" "rough" "+")
triple11
Harry is round.
("Harry" "is" "round" "+")
triple12
((triple10) -> (rule6 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
((triple7 triple6) -> (rule4 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is not red.
("Erin" "is" "red" "-")
((((triple7 triple6) -> (rule4 % int2))) -> (rule1 % int1))
Erin is not red.
("Erin" "is" "red" "-")
int1
Erin is big.
("Erin" "is" "big" "+")
int2