Bob is cold. Bob is quiet. Bob is smart. Charlie is cold. Charlie is red. Erin is cold. Erin is quiet. Erin is red. Fiona is quiet. Fiona is smart. If something is quiet then it is smart. All red things are quiet. Smart, quiet things are round.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is red.
("Erin" "is" "red" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
If something is quiet then it is smart.
((("something" "is" "quiet" "+")) -> ("something" "is" "smart" "+"))
All red things are quiet.
((("something" "is" "red" "+")) -> ("something" "is" "quiet" "+"))
Smart, quiet things are round.
((("something" "is" "smart" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "round" "+"))
Erin is quiet.
True
1
proof
[(triple7 OR ((triple8) -> rule2))]
("Erin" "is" "quiet" "+")
triple7
((triple8) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Bob is not smart.
False
1
inv-proof
[(triple3 OR ((triple2) -> rule1))]
("Bob" "is" "smart" "-")
triple3
((triple2) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Erin is smart.
True
2
proof
[(((triple7) -> rule1) OR ((((triple8) -> rule2)) -> rule1))]
("Erin" "is" "smart" "+")
((triple7) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((((triple8) -> (rule2 % int2))) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is not smart.
False
2
inv-proof
[(((triple7) -> rule1) OR ((((triple8) -> rule2)) -> rule1))]
("Erin" "is" "smart" "-")
((triple7) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((((triple8) -> (rule2 % int2))) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is round.
True
4
proof
[(((((triple7) -> rule1) triple7) -> rule3) OR ((((triple7) -> rule1) ((triple8) -> rule2)) -> rule3) OR ((((((triple8) -> rule2)) -> rule1) triple7) -> rule3) OR ((((((triple8) -> rule2)) -> rule1) ((triple8) -> rule2)) -> rule3))]
("Erin" "is" "round" "+")
((((triple7) -> (rule1 % int2)) triple7) -> (rule3 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
((((triple7) -> (rule1 % int3)) ((triple8) -> (rule2 % int2))) -> (rule3 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
((((((triple8) -> (rule2 % int3))) -> (rule1 % int2)) triple7) -> (rule3 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
((((((triple8) -> (rule2 % int3))) -> (rule1 % int2)) ((triple8) -> (rule2 % int3))) -> (rule3 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
Erin is not round.
False
4
inv-proof
[(((((triple7) -> rule1) triple7) -> rule3) OR ((((triple7) -> rule1) ((triple8) -> rule2)) -> rule3) OR ((((((triple8) -> rule2)) -> rule1) triple7) -> rule3) OR ((((((triple8) -> rule2)) -> rule1) ((triple8) -> rule2)) -> rule3))]
("Erin" "is" "round" "-")
((((triple7) -> (rule1 % int2)) triple7) -> (rule3 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
((((triple7) -> (rule1 % int3)) ((triple8) -> (rule2 % int2))) -> (rule3 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
((((((triple8) -> (rule2 % int3))) -> (rule1 % int2)) triple7) -> (rule3 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
((((((triple8) -> (rule2 % int3))) -> (rule1 % int2)) ((triple8) -> (rule2 % int3))) -> (rule3 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
Charlie is round.
True
6
proof
[(((((((triple5) -> rule2)) -> rule1) ((triple5) -> rule2)) -> rule3))]
("Charlie" "is" "round" "+")
((((((triple5) -> (rule2 % int3))) -> (rule1 % int2)) ((triple5) -> (rule2 % int3))) -> (rule3 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Charlie is not round.
False
6
inv-proof
[(((((((triple5) -> rule2)) -> rule1) ((triple5) -> rule2)) -> rule3))]
("Charlie" "is" "round" "-")
((((((triple5) -> (rule2 % int3))) -> (rule1 % int2)) ((triple5) -> (rule2 % int3))) -> (rule3 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Erin is not blue.
Unknown
inv-random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "-")
Fiona is red.
Unknown
random
[@0: Fiona is red.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "red" "+")
Charlie is not young.
Unknown
inv-random
[@0: Charlie is young.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "young" "-")
Bob is red.
Unknown
random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "+")
Bob is not young.
Unknown
inv-random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "-")
Charlie is blue.
Unknown
random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "+")
Bob is not blue.
Unknown
inv-random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "-")
Fiona is blue.
Unknown
random
[@0: Fiona is blue.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "blue" "+")
@0: Bob is cold.[(triple1)] Bob is quiet.[(triple2)] Bob is smart.[(triple3 OR ((triple2) -> rule1))] Charlie is cold.[(triple4)] Charlie is red.[(triple5)] Erin is cold.[(triple6)] Erin is quiet.[(triple7 OR ((triple8) -> rule2))] Erin is red.[(triple8)] Fiona is quiet.[(triple9)] Fiona is smart.[(triple10 OR ((triple9) -> rule1))] @1: Bob is round.[(((triple3 triple2) -> rule3) OR ((((triple2) -> rule1) triple2) -> rule3))] Charlie is quiet.[(((triple5) -> rule2))] Erin is smart.[(((triple7) -> rule1) OR ((((triple8) -> rule2)) -> rule1))] Fiona is round.[(((triple10 triple9) -> rule3) OR ((((triple9) -> rule1) triple9) -> rule3))] @2: Charlie is smart.[(((((triple5) -> rule2)) -> rule1))] Erin is round.[(((((triple7) -> rule1) triple7) -> rule3) OR ((((triple7) -> rule1) ((triple8) -> rule2)) -> rule3) OR ((((((triple8) -> rule2)) -> rule1) triple7) -> rule3) OR ((((((triple8) -> rule2)) -> rule1) ((triple8) -> rule2)) -> rule3))] @3: Charlie is round.[(((((((triple5) -> rule2)) -> rule1) ((triple5) -> rule2)) -> rule3))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Bob is quiet.
("Bob" "is" "quiet" "+")
triple2
Bob is smart.
("Bob" "is" "smart" "+")
triple3
((triple2) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple4
Charlie is red.
("Charlie" "is" "red" "+")
triple5
Erin is cold.
("Erin" "is" "cold" "+")
triple6
Erin is quiet.
("Erin" "is" "quiet" "+")
triple7
((triple8) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
triple8
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple9
Fiona is smart.
("Fiona" "is" "smart" "+")
triple10
((triple9) -> (rule1 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
((triple3 triple2) -> (rule3 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
((((triple2) -> (rule1 % int2)) triple2) -> (rule3 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple5) -> (rule2 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
((triple7) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((((triple8) -> (rule2 % int2))) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
((triple10 triple9) -> (rule3 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
((((triple9) -> (rule1 % int2)) triple9) -> (rule3 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
((((triple5) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
((((triple7) -> (rule1 % int2)) triple7) -> (rule3 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
((((triple7) -> (rule1 % int3)) ((triple8) -> (rule2 % int2))) -> (rule3 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
((((((triple8) -> (rule2 % int3))) -> (rule1 % int2)) triple7) -> (rule3 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
((((((triple8) -> (rule2 % int3))) -> (rule1 % int2)) ((triple8) -> (rule2 % int3))) -> (rule3 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
Charlie is round.
("Charlie" "is" "round" "+")
((((((triple5) -> (rule2 % int3))) -> (rule1 % int2)) ((triple5) -> (rule2 % int3))) -> (rule3 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3