Erin is big. Erin is smart. Erin is not white. Harry is big. Harry is red. Harry is rough. Harry is white. All white, smart things are not cold. All big, smart things are not cold. Rough, white things are smart. If something is young and not big then it is smart. If Harry is big and Harry is white then Harry is not young. If Harry is cold then Harry is not rough.
Erin is big.
("Erin" "is" "big" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is not white.
("Erin" "is" "white" "-")
Harry is big.
("Harry" "is" "big" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is white.
("Harry" "is" "white" "+")
All white, smart things are not cold.
((("something" "is" "white" "+") ("something" "is" "smart" "+")) -> ("something" "is" "cold" "-"))
All big, smart things are not cold.
((("something" "is" "big" "+") ("something" "is" "smart" "+")) -> ("something" "is" "cold" "-"))
Rough, white things are smart.
((("something" "is" "rough" "+") ("something" "is" "white" "+")) -> ("something" "is" "smart" "+"))
If something is young and not big then it is smart.
((("something" "is" "young" "+") ("something" "is" "big" "~")) -> ("something" "is" "smart" "+"))
If Harry is big and Harry is white then Harry is not young.
((("Harry" "is" "big" "+") ("Harry" "is" "white" "+")) -> ("Harry" "is" "young" "-"))
If Harry is cold then Harry is not rough.
((("Harry" "is" "cold" "+")) -> ("Harry" "is" "rough" "-"))
Erin is not white.
True
1
proof
[(triple3)]
("Erin" "is" "white" "-")
triple3
Erin is not big.
False
1
inv-proof
[(triple1)]
("Erin" "is" "big" "-")
triple1
Erin is not cold.
True
3
proof
[(((triple1 triple2) -> rule2))]
("Erin" "is" "cold" "-")
((triple1 triple2) -> (rule2 % int1))
Erin is not cold.
("Erin" "is" "cold" "-")
int1
Harry is not smart.
False
3
inv-proof
[(((triple6 triple7) -> rule3))]
("Harry" "is" "smart" "-")
((triple6 triple7) -> (rule3 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is not cold.
True
5
proof
[(((triple4 ((triple6 triple7) -> rule3)) -> rule2) OR ((triple7 ((triple6 triple7) -> rule3)) -> rule1))]
("Harry" "is" "cold" "-")
((triple4 ((triple6 triple7) -> (rule3 % int2))) -> (rule2 % int1))
Harry is not cold.
("Harry" "is" "cold" "-")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
((triple7 ((triple6 triple7) -> (rule3 % int2))) -> (rule1 % int1))
Harry is not cold.
("Harry" "is" "cold" "-")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is cold.
False
5
inv-proof
[(((triple4 ((triple6 triple7) -> rule3)) -> rule2) OR ((triple7 ((triple6 triple7) -> rule3)) -> rule1))]
("Harry" "is" "cold" "+")
((triple4 ((triple6 triple7) -> (rule3 % int2))) -> (rule2 % int1))
Harry is not cold.
("Harry" "is" "cold" "-")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
((triple7 ((triple6 triple7) -> (rule3 % int2))) -> (rule1 % int1))
Harry is not cold.
("Harry" "is" "cold" "-")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Erin is not rough.
Unknown
inv-random
[@0: Erin is rough.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "rough" "-")
Erin is young.
Unknown
random
[@0: Erin is young.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "young" "+")
@0: Erin is big.[(triple1)] Erin is not white.[(triple3)] Erin is smart.[(triple2)] Harry is big.[(triple4)] Harry is red.[(triple5)] Harry is rough.[(triple6)] Harry is white.[(triple7)] @1: Erin is not cold.[(((triple1 triple2) -> rule2))] Harry is not young.[(((triple4 triple7) -> rule5))] Harry is smart.[(((triple6 triple7) -> rule3))] @2: Harry is not cold.[(((triple4 ((triple6 triple7) -> rule3)) -> rule2) OR ((triple7 ((triple6 triple7) -> rule3)) -> rule1))]
Erin is big.
("Erin" "is" "big" "+")
triple1
Erin is not white.
("Erin" "is" "white" "-")
triple3
Erin is smart.
("Erin" "is" "smart" "+")
triple2
Harry is big.
("Harry" "is" "big" "+")
triple4
Harry is red.
("Harry" "is" "red" "+")
triple5
Harry is rough.
("Harry" "is" "rough" "+")
triple6
Harry is white.
("Harry" "is" "white" "+")
triple7
Erin is not cold.
("Erin" "is" "cold" "-")
((triple1 triple2) -> (rule2 % int1))
Erin is not cold.
("Erin" "is" "cold" "-")
int1
Harry is not young.
("Harry" "is" "young" "-")
((triple4 triple7) -> (rule5 % int1))
Harry is not young.
("Harry" "is" "young" "-")
int1
Harry is smart.
("Harry" "is" "smart" "+")
((triple6 triple7) -> (rule3 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is not cold.
("Harry" "is" "cold" "-")
((triple4 ((triple6 triple7) -> (rule3 % int2))) -> (rule2 % int1))
Harry is not cold.
("Harry" "is" "cold" "-")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
((triple7 ((triple6 triple7) -> (rule3 % int2))) -> (rule1 % int1))
Harry is not cold.
("Harry" "is" "cold" "-")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2