Erin is big. Erin is blue. Erin is cold. Erin is kind. Gary is big. Gary is blue. Gary is cold. Gary is kind. Gary is nice. Gary is white. Harry is big. Harry is blue. Harry is green. Harry is kind. Harry is nice. All big things are green. Big things are green. If something is white then it is nice. If something is cold then it is kind. Green, cold things are big. All green things are kind.
Erin is big.
("Erin" "is" "big" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is white.
("Gary" "is" "white" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is nice.
("Harry" "is" "nice" "+")
All big things are green.
((("something" "is" "big" "+")) -> ("something" "is" "green" "+"))
Big things are green.
((("something" "is" "big" "+")) -> ("something" "is" "green" "+"))
If something is white then it is nice.
((("something" "is" "white" "+")) -> ("something" "is" "nice" "+"))
If something is cold then it is kind.
((("something" "is" "cold" "+")) -> ("something" "is" "kind" "+"))
Green, cold things are big.
((("something" "is" "green" "+") ("something" "is" "cold" "+")) -> ("something" "is" "big" "+"))
All green things are kind.
((("something" "is" "green" "+")) -> ("something" "is" "kind" "+"))
Erin is kind.
True
1
proof
[(triple4 OR ((triple3) -> rule4) OR ((((triple1) -> rule1)) -> rule6) OR ((((triple1) -> rule2)) -> rule6))]
("Erin" "is" "kind" "+")
triple4
((triple3) -> (rule4 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
((((triple1) -> (rule1 % int2))) -> (rule6 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
((((triple1) -> (rule2 % int2))) -> (rule6 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Gary is not kind.
False
1
inv-proof
[(triple8 OR ((triple7) -> rule4) OR ((((triple5) -> rule1)) -> rule6) OR ((((triple5) -> rule2)) -> rule6))]
("Gary" "is" "kind" "-")
triple8
((triple7) -> (rule4 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
((((triple5) -> (rule1 % int2))) -> (rule6 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
((((triple5) -> (rule2 % int2))) -> (rule6 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is green.
True
2
proof
[(((triple5) -> rule1) OR ((triple5) -> rule2))]
("Gary" "is" "green" "+")
((triple5) -> (rule1 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
((triple5) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Erin is not green.
False
2
inv-proof
[(((triple1) -> rule1) OR ((triple1) -> rule2))]
("Erin" "is" "green" "-")
((triple1) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
((triple1) -> (rule2 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is not nice.
Unknown
inv-rconc
[@1: Erin is nice.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Erin" "is" "nice" "-")
Harry is cold.
Unknown
random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "+")
Harry is not white.
Unknown
inv-random
[@0: Harry is white.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "white" "-")
Erin is white.
Unknown
random
[@0: Erin is white.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "white" "+")
@0: Erin is big.[(triple1)] Erin is blue.[(triple2)] Erin is cold.[(triple3)] Erin is kind.[(triple4 OR ((triple3) -> rule4) OR ((((triple1) -> rule1)) -> rule6) OR ((((triple1) -> rule2)) -> rule6))] Gary is big.[(triple5)] Gary is blue.[(triple6)] Gary is cold.[(triple7)] Gary is kind.[(triple8 OR ((triple7) -> rule4) OR ((((triple5) -> rule1)) -> rule6) OR ((((triple5) -> rule2)) -> rule6))] Gary is nice.[(triple9 OR ((triple10) -> rule3))] Gary is white.[(triple10)] Harry is big.[(triple11)] Harry is blue.[(triple12)] Harry is green.[(triple13 OR ((triple11) -> rule1) OR ((triple11) -> rule2))] Harry is kind.[(triple14 OR ((triple13) -> rule6) OR ((((triple11) -> rule1)) -> rule6) OR ((((triple11) -> rule2)) -> rule6))] Harry is nice.[(triple15)] @1: Erin is green.[(((triple1) -> rule1) OR ((triple1) -> rule2))] Gary is green.[(((triple5) -> rule1) OR ((triple5) -> rule2))]
Erin is big.
("Erin" "is" "big" "+")
triple1
Erin is blue.
("Erin" "is" "blue" "+")
triple2
Erin is cold.
("Erin" "is" "cold" "+")
triple3
Erin is kind.
("Erin" "is" "kind" "+")
triple4
((triple3) -> (rule4 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
((((triple1) -> (rule1 % int2))) -> (rule6 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
((((triple1) -> (rule2 % int2))) -> (rule6 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
triple5
Gary is blue.
("Gary" "is" "blue" "+")
triple6
Gary is cold.
("Gary" "is" "cold" "+")
triple7
Gary is kind.
("Gary" "is" "kind" "+")
triple8
((triple7) -> (rule4 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
((((triple5) -> (rule1 % int2))) -> (rule6 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
((((triple5) -> (rule2 % int2))) -> (rule6 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
triple9
((triple10) -> (rule3 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
triple10
Harry is big.
("Harry" "is" "big" "+")
triple11
Harry is blue.
("Harry" "is" "blue" "+")
triple12
Harry is green.
("Harry" "is" "green" "+")
triple13
((triple11) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
((triple11) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
triple14
((triple13) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((((triple11) -> (rule1 % int2))) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
((((triple11) -> (rule2 % int2))) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
triple15
Erin is green.
("Erin" "is" "green" "+")
((triple1) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
((triple1) -> (rule2 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
((triple5) -> (rule1 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
((triple5) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1