Charlie is big. Charlie is blue. Charlie is quiet. Charlie is rough. Charlie is smart. Charlie is young. Erin is blue. Erin is quiet. Erin is rough. Erin is smart. Erin is young. Gary is blue. Blue, quiet people are smart. If someone is big then they are red. All red people are smart. Red, smart people are big. Blue people are big. All rough, young people are smart.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is young.
("Erin" "is" "young" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Blue, quiet people are smart.
((("someone" "is" "blue" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "smart" "+"))
If someone is big then they are red.
((("someone" "is" "big" "+")) -> ("someone" "is" "red" "+"))
All red people are smart.
((("someone" "is" "red" "+")) -> ("someone" "is" "smart" "+"))
Red, smart people are big.
((("someone" "is" "red" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "big" "+"))
Blue people are big.
((("someone" "is" "blue" "+")) -> ("someone" "is" "big" "+"))
All rough, young people are smart.
((("someone" "is" "rough" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "smart" "+"))
Charlie is blue.
True
1
proof
[(triple2)]
("Charlie" "is" "blue" "+")
triple2
Charlie is not big.
False
1
inv-proof
[(triple1 OR ((triple2) -> rule5))]
("Charlie" "is" "big" "-")
triple1
((triple2) -> (rule5 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Erin is big.
True
2
proof
[(((triple7) -> rule5))]
("Erin" "is" "big" "+")
((triple7) -> (rule5 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is not big.
False
2
inv-proof
[(((triple7) -> rule5))]
("Erin" "is" "big" "-")
((triple7) -> (rule5 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is red.
True
3
proof
[(((((triple7) -> rule5)) -> rule2))]
("Erin" "is" "red" "+")
((((triple7) -> (rule5 % int2))) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is not red.
False
3
inv-proof
[(((((triple7) -> rule5)) -> rule2))]
("Erin" "is" "red" "-")
((((triple7) -> (rule5 % int2))) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Gary is smart.
True
4
proof
[(((((((triple12) -> rule5)) -> rule2)) -> rule3))]
("Gary" "is" "smart" "+")
((((((triple12) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
Gary is not smart.
False
4
inv-proof
[(((((((triple12) -> rule5)) -> rule2)) -> rule3))]
("Gary" "is" "smart" "-")
((((((triple12) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
Gary is not young.
Unknown
inv-random
[@0: Gary is young.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "young" "-")
Gary is quiet.
Unknown
random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "+")
@0: Charlie is big.[(triple1 OR ((triple2) -> rule5))] Charlie is blue.[(triple2)] Charlie is quiet.[(triple3)] Charlie is rough.[(triple4)] Charlie is smart.[(triple5 OR ((triple2 triple3) -> rule1) OR ((triple4 triple6) -> rule6) OR ((((triple1) -> rule2)) -> rule3) OR ((((((triple2) -> rule5)) -> rule2)) -> rule3))] Charlie is young.[(triple6)] Erin is blue.[(triple7)] Erin is quiet.[(triple8)] Erin is rough.[(triple9)] Erin is smart.[(triple10 OR ((triple7 triple8) -> rule1) OR ((triple9 triple11) -> rule6) OR ((((((triple7) -> rule5)) -> rule2)) -> rule3))] Erin is young.[(triple11)] Gary is blue.[(triple12)] @1: Charlie is red.[(((triple1) -> rule2) OR ((((triple2) -> rule5)) -> rule2))] Erin is big.[(((triple7) -> rule5))] Gary is big.[(((triple12) -> rule5))] @2: Erin is red.[(((((triple7) -> rule5)) -> rule2))] Gary is red.[(((((triple12) -> rule5)) -> rule2))] @3: Gary is smart.[(((((((triple12) -> rule5)) -> rule2)) -> rule3))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
((triple2) -> (rule5 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
triple2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple3
Charlie is rough.
("Charlie" "is" "rough" "+")
triple4
Charlie is smart.
("Charlie" "is" "smart" "+")
triple5
((triple2 triple3) -> (rule1 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
((triple4 triple6) -> (rule6 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
((((((triple2) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Charlie is young.
("Charlie" "is" "young" "+")
triple6
Erin is blue.
("Erin" "is" "blue" "+")
triple7
Erin is quiet.
("Erin" "is" "quiet" "+")
triple8
Erin is rough.
("Erin" "is" "rough" "+")
triple9
Erin is smart.
("Erin" "is" "smart" "+")
triple10
((triple7 triple8) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((triple9 triple11) -> (rule6 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((((((triple7) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Erin is young.
("Erin" "is" "young" "+")
triple11
Gary is blue.
("Gary" "is" "blue" "+")
triple12
Charlie is red.
("Charlie" "is" "red" "+")
((triple1) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
((((triple2) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
((triple7) -> (rule5 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
((triple12) -> (rule5 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
((((triple7) -> (rule5 % int2))) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
((((triple12) -> (rule5 % int2))) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
((((((triple12) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3