Bob is rough. Bob is round. Charlie is rough. Charlie is white. Erin is big. Erin is blue. Erin is cold. Erin is kind. Erin is rough. Erin is round. Erin is white. Harry is blue. Harry is cold. Harry is rough. Harry is round. Harry is white. If Charlie is white then Charlie is round. If someone is cold and round then they are white. If Erin is rough and Erin is kind then Erin is big. If someone is big then they are kind. If someone is blue and cold then they are big. If Erin is cold and Erin is blue then Erin is kind.
Bob is rough.
("Bob" "is" "rough" "+")
Bob is round.
("Bob" "is" "round" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is white.
("Erin" "is" "white" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is white.
("Harry" "is" "white" "+")
If Charlie is white then Charlie is round.
((("Charlie" "is" "white" "+")) -> ("Charlie" "is" "round" "+"))
If someone is cold and round then they are white.
((("someone" "is" "cold" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "white" "+"))
If Erin is rough and Erin is kind then Erin is big.
((("Erin" "is" "rough" "+") ("Erin" "is" "kind" "+")) -> ("Erin" "is" "big" "+"))
If someone is big then they are kind.
((("someone" "is" "big" "+")) -> ("someone" "is" "kind" "+"))
If someone is blue and cold then they are big.
((("someone" "is" "blue" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "big" "+"))
If Erin is cold and Erin is blue then Erin is kind.
((("Erin" "is" "cold" "+") ("Erin" "is" "blue" "+")) -> ("Erin" "is" "kind" "+"))
Erin is cold.
True
1
proof
[(triple7)]
("Erin" "is" "cold" "+")
triple7
Bob is not rough.
False
1
inv-proof
[(triple1)]
("Bob" "is" "rough" "-")
triple1
Harry is big.
True
3
proof
[(((triple12 triple13) -> rule5))]
("Harry" "is" "big" "+")
((triple12 triple13) -> (rule5 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is not big.
False
3
inv-proof
[(((triple12 triple13) -> rule5))]
("Harry" "is" "big" "-")
((triple12 triple13) -> (rule5 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is kind.
True
4
proof
[(((((triple12 triple13) -> rule5)) -> rule4))]
("Harry" "is" "kind" "+")
((((triple12 triple13) -> (rule5 % int2))) -> (rule4 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is not kind.
False
4
inv-proof
[(((((triple12 triple13) -> rule5)) -> rule4))]
("Harry" "is" "kind" "-")
((((triple12 triple13) -> (rule5 % int2))) -> (rule4 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Charlie is not big.
Unknown
inv-rconc
[@1: Charlie is big.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Charlie" "is" "big" "-")
Charlie is kind.
Unknown
rconc
[@2: Charlie is kind.[CWA. Example of deepest failure = (rule4 <- rule5 <- FAIL)]]
("Charlie" "is" "kind" "+")
Bob is not white.
Unknown
inv-rconc
[@1: Bob is white.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "white" "-")
Charlie is cold.
Unknown
random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "+")
Charlie is not blue.
Unknown
inv-random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "-")
Bob is blue.
Unknown
random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "+")
@0: Bob is rough.[(triple1)] Bob is round.[(triple2)] Charlie is rough.[(triple3)] Charlie is white.[(triple4)] Erin is big.[(triple5 OR ((triple6 triple7) -> rule5) OR ((triple9 triple8) -> rule3) OR ((triple9 ((triple7 triple6) -> rule6)) -> rule3))] Erin is blue.[(triple6)] Erin is cold.[(triple7)] Erin is kind.[(triple8 OR ((triple5) -> rule4) OR ((triple7 triple6) -> rule6) OR ((((triple6 triple7) -> rule5)) -> rule4))] Erin is rough.[(triple9)] Erin is round.[(triple10)] Erin is white.[(triple11 OR ((triple7 triple10) -> rule2))] Harry is blue.[(triple12)] Harry is cold.[(triple13)] Harry is rough.[(triple14)] Harry is round.[(triple15)] Harry is white.[(triple16 OR ((triple13 triple15) -> rule2))] @1: Charlie is round.[(((triple4) -> rule1))] Harry is big.[(((triple12 triple13) -> rule5))] @2: Harry is kind.[(((((triple12 triple13) -> rule5)) -> rule4))]
Bob is rough.
("Bob" "is" "rough" "+")
triple1
Bob is round.
("Bob" "is" "round" "+")
triple2
Charlie is rough.
("Charlie" "is" "rough" "+")
triple3
Charlie is white.
("Charlie" "is" "white" "+")
triple4
Erin is big.
("Erin" "is" "big" "+")
triple5
((triple6 triple7) -> (rule5 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
((triple9 triple8) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
((triple9 ((triple7 triple6) -> (rule6 % int2))) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
triple6
Erin is cold.
("Erin" "is" "cold" "+")
triple7
Erin is kind.
("Erin" "is" "kind" "+")
triple8
((triple5) -> (rule4 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
((triple7 triple6) -> (rule6 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
((((triple6 triple7) -> (rule5 % int2))) -> (rule4 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
triple9
Erin is round.
("Erin" "is" "round" "+")
triple10
Erin is white.
("Erin" "is" "white" "+")
triple11
((triple7 triple10) -> (rule2 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
triple12
Harry is cold.
("Harry" "is" "cold" "+")
triple13
Harry is rough.
("Harry" "is" "rough" "+")
triple14
Harry is round.
("Harry" "is" "round" "+")
triple15
Harry is white.
("Harry" "is" "white" "+")
triple16
((triple13 triple15) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
((triple4) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
((triple12 triple13) -> (rule5 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
((((triple12 triple13) -> (rule5 % int2))) -> (rule4 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2