Bob is green. Charlie is not big. Charlie is cold. Charlie is smart. Charlie is young. Erin is big. Erin is not green. Erin is smart. Erin is white. Erin is young. Fiona is green. Fiona is white. If something is smart then it is white. If something is red and not young then it is not white. All red, big things are white. If Bob is smart then Bob is cold. All green things are big. If something is young and green then it is smart. If something is big then it is smart. If Erin is green then Erin is big.
Bob is green.
("Bob" "is" "green" "+")
Charlie is not big.
("Charlie" "is" "big" "-")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is not green.
("Erin" "is" "green" "-")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is white.
("Erin" "is" "white" "+")
Erin is young.
("Erin" "is" "young" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is white.
("Fiona" "is" "white" "+")
If something is smart then it is white.
((("something" "is" "smart" "+")) -> ("something" "is" "white" "+"))
If something is red and not young then it is not white.
((("something" "is" "red" "+") ("something" "is" "young" "~")) -> ("something" "is" "white" "-"))
All red, big things are white.
((("something" "is" "red" "+") ("something" "is" "big" "+")) -> ("something" "is" "white" "+"))
If Bob is smart then Bob is cold.
((("Bob" "is" "smart" "+")) -> ("Bob" "is" "cold" "+"))
All green things are big.
((("something" "is" "green" "+")) -> ("something" "is" "big" "+"))
If something is young and green then it is smart.
((("something" "is" "young" "+") ("something" "is" "green" "+")) -> ("something" "is" "smart" "+"))
If something is big then it is smart.
((("something" "is" "big" "+")) -> ("something" "is" "smart" "+"))
If Erin is green then Erin is big.
((("Erin" "is" "green" "+")) -> ("Erin" "is" "big" "+"))
Charlie is young.
True
1
proof
[(triple5)]
("Charlie" "is" "young" "+")
triple5
Erin is not smart.
False
1
inv-proof
[(triple8 OR ((triple6) -> rule7))]
("Erin" "is" "smart" "-")
triple8
((triple6) -> (rule7 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Charlie is white.
True
2
proof
[(((triple4) -> rule1))]
("Charlie" "is" "white" "+")
((triple4) -> (rule1 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is not white.
False
2
inv-proof
[(((triple4) -> rule1))]
("Charlie" "is" "white" "-")
((triple4) -> (rule1 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Bob is smart.
True
3
proof
[(((((triple1) -> rule5)) -> rule7))]
("Bob" "is" "smart" "+")
((((triple1) -> (rule5 % int2))) -> (rule7 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is not smart.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule7))]
("Bob" "is" "smart" "-")
((((triple1) -> (rule5 % int2))) -> (rule7 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is cold.
True
4
proof
[(((((((triple1) -> rule5)) -> rule7)) -> rule4))]
("Bob" "is" "cold" "+")
((((((triple1) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is not white.
False
4
inv-proof
[(((((((triple1) -> rule5)) -> rule7)) -> rule1))]
("Bob" "is" "white" "-")
((((((triple1) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Fiona is not young.
Unknown
inv-random
[@0: Fiona is young.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "young" "-")
Erin is red.
Unknown
random
[@0: Erin is red.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "red" "+")
Fiona is not red.
Unknown
inv-random
[@0: Fiona is red.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "red" "-")
Erin is cold.
Unknown
random
[@0: Erin is cold.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "cold" "+")
Charlie is not red.
Unknown
inv-random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "-")
Bob is red.
Unknown
random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "+")
Fiona is not cold.
Unknown
inv-random
[@0: Fiona is cold.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "cold" "-")
Charlie is green.
Unknown
random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "+")
@0: Bob is green.[(triple1)] Charlie is cold.[(triple3)] Charlie is not big.[(triple2)] Charlie is smart.[(triple4)] Charlie is young.[(triple5)] Erin is big.[(triple6)] Erin is not green.[(triple7)] Erin is smart.[(triple8 OR ((triple6) -> rule7))] Erin is white.[(triple9 OR ((triple8) -> rule1) OR ((((triple6) -> rule7)) -> rule1))] Erin is young.[(triple10)] Fiona is green.[(triple11)] Fiona is white.[(triple12 OR ((((((triple11) -> rule5)) -> rule7)) -> rule1))] @1: Bob is big.[(((triple1) -> rule5))] Charlie is white.[(((triple4) -> rule1))] Fiona is big.[(((triple11) -> rule5))] @2: Bob is smart.[(((((triple1) -> rule5)) -> rule7))] Fiona is smart.[(((((triple11) -> rule5)) -> rule7))] @3: Bob is cold.[(((((((triple1) -> rule5)) -> rule7)) -> rule4))] Bob is white.[(((((((triple1) -> rule5)) -> rule7)) -> rule1))]
Bob is green.
("Bob" "is" "green" "+")
triple1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple3
Charlie is not big.
("Charlie" "is" "big" "-")
triple2
Charlie is smart.
("Charlie" "is" "smart" "+")
triple4
Charlie is young.
("Charlie" "is" "young" "+")
triple5
Erin is big.
("Erin" "is" "big" "+")
triple6
Erin is not green.
("Erin" "is" "green" "-")
triple7
Erin is smart.
("Erin" "is" "smart" "+")
triple8
((triple6) -> (rule7 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
triple9
((triple8) -> (rule1 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
((((triple6) -> (rule7 % int2))) -> (rule1 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
triple10
Fiona is green.
("Fiona" "is" "green" "+")
triple11
Fiona is white.
("Fiona" "is" "white" "+")
triple12
((((((triple11) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
int3
Bob is big.
("Bob" "is" "big" "+")
((triple1) -> (rule5 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
((triple4) -> (rule1 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
((triple11) -> (rule5 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
((((triple1) -> (rule5 % int2))) -> (rule7 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
((((triple11) -> (rule5 % int2))) -> (rule7 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
((((((triple1) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
((((((triple1) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3