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