Charlie is big. Charlie is nice. Charlie is white. Charlie is young. Erin is cold. Erin is smart. Erin is white. Gary is big. Gary is cold. Gary is nice. Gary is rough. Gary is smart. Gary is white. Harry is cold. Harry is nice. Harry is white. Big people are cold. All cold people are smart.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is white.
("Erin" "is" "white" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is white.
("Gary" "is" "white" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is white.
("Harry" "is" "white" "+")
Big people are cold.
((("someone" "is" "big" "+")) -> ("someone" "is" "cold" "+"))
All cold people are smart.
((("someone" "is" "cold" "+")) -> ("someone" "is" "smart" "+"))
Gary is cold.
True
1
proof
[(triple9 OR ((triple8) -> rule1))]
("Gary" "is" "cold" "+")
triple9
((triple8) -> (rule1 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Charlie is not nice.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "nice" "-")
triple2
Charlie is cold.
True
2
proof
[(((triple1) -> rule1))]
("Charlie" "is" "cold" "+")
((triple1) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Harry is not smart.
False
2
inv-proof
[(((triple14) -> rule2))]
("Harry" "is" "smart" "-")
((triple14) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Charlie is smart.
True
3
proof
[(((((triple1) -> rule1)) -> rule2))]
("Charlie" "is" "smart" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is not smart.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule2))]
("Charlie" "is" "smart" "-")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Erin is not young.
Unknown
inv-random
[@0: Erin is young.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "young" "-")
Erin is nice.
Unknown
random
[@0: Erin is nice.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "nice" "+")
Harry is not rough.
Unknown
inv-random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "-")
Erin is big.
Unknown
random
[@0: Erin is big.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "big" "+")
Erin is not rough.
Unknown
inv-random
[@0: Erin is rough.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "rough" "-")
Harry is young.
Unknown
random
[@0: Harry is young.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "young" "+")
@0: Charlie is big.[(triple1)] Charlie is nice.[(triple2)] Charlie is white.[(triple3)] Charlie is young.[(triple4)] Erin is cold.[(triple5)] Erin is smart.[(triple6 OR ((triple5) -> rule2))] Erin is white.[(triple7)] Gary is big.[(triple8)] Gary is cold.[(triple9 OR ((triple8) -> rule1))] Gary is nice.[(triple10)] Gary is rough.[(triple11)] Gary is smart.[(triple12 OR ((triple9) -> rule2) OR ((((triple8) -> rule1)) -> rule2))] Gary is white.[(triple13)] Harry is cold.[(triple14)] Harry is nice.[(triple15)] Harry is white.[(triple16)] @1: Charlie is cold.[(((triple1) -> rule1))] Harry is smart.[(((triple14) -> rule2))] @2: Charlie is smart.[(((((triple1) -> rule1)) -> rule2))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Charlie is nice.
("Charlie" "is" "nice" "+")
triple2
Charlie is white.
("Charlie" "is" "white" "+")
triple3
Charlie is young.
("Charlie" "is" "young" "+")
triple4
Erin is cold.
("Erin" "is" "cold" "+")
triple5
Erin is smart.
("Erin" "is" "smart" "+")
triple6
((triple5) -> (rule2 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
triple7
Gary is big.
("Gary" "is" "big" "+")
triple8
Gary is cold.
("Gary" "is" "cold" "+")
triple9
((triple8) -> (rule1 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
triple10
Gary is rough.
("Gary" "is" "rough" "+")
triple11
Gary is smart.
("Gary" "is" "smart" "+")
triple12
((triple9) -> (rule2 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
((((triple8) -> (rule1 % int2))) -> (rule2 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
triple13
Harry is cold.
("Harry" "is" "cold" "+")
triple14
Harry is nice.
("Harry" "is" "nice" "+")
triple15
Harry is white.
("Harry" "is" "white" "+")
triple16
Charlie is cold.
("Charlie" "is" "cold" "+")
((triple1) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
((triple14) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2