Anne is white. Bob is blue. Bob is green. Bob is nice. Bob is rough. Charlie is big. Charlie is green. Charlie is nice. Charlie is rough. Charlie is smart. Charlie is white. Erin is big. Erin is green. Erin is smart. Erin is white. All rough things are white. Big things are white. If Charlie is big then Charlie is rough. All white, blue things are big. If something is big and not rough then it is not smart. If something is big then it is smart.
Anne is white.
("Anne" "is" "white" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is white.
("Erin" "is" "white" "+")
All rough things are white.
((("something" "is" "rough" "+")) -> ("something" "is" "white" "+"))
Big things are white.
((("something" "is" "big" "+")) -> ("something" "is" "white" "+"))
If Charlie is big then Charlie is rough.
((("Charlie" "is" "big" "+")) -> ("Charlie" "is" "rough" "+"))
All white, blue things are big.
((("something" "is" "white" "+") ("something" "is" "blue" "+")) -> ("something" "is" "big" "+"))
If something is big and not rough then it is not smart.
((("something" "is" "big" "+") ("something" "is" "rough" "~")) -> ("something" "is" "smart" "-"))
If something is big then it is smart.
((("something" "is" "big" "+")) -> ("something" "is" "smart" "+"))
Charlie is green.
True
1
proof
[(triple7)]
("Charlie" "is" "green" "+")
triple7
Erin is not white.
False
1
inv-proof
[(triple15 OR ((triple12) -> rule2))]
("Erin" "is" "white" "-")
triple15
((triple12) -> (rule2 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Bob is white.
True
2
proof
[(((triple5) -> rule1))]
("Bob" "is" "white" "+")
((triple5) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is not white.
False
2
inv-proof
[(((triple5) -> rule1))]
("Bob" "is" "white" "-")
((triple5) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is big.
True
4
proof
[(((((triple5) -> rule1) triple2) -> rule4))]
("Bob" "is" "big" "+")
((((triple5) -> (rule1 % int2)) triple2) -> (rule4 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is not big.
False
4
inv-proof
[(((((triple5) -> rule1) triple2) -> rule4))]
("Bob" "is" "big" "-")
((((triple5) -> (rule1 % int2)) triple2) -> (rule4 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is smart.
True
5
proof
[(((((((triple5) -> rule1) triple2) -> rule4)) -> rule6))]
("Bob" "is" "smart" "+")
((((((triple5) -> (rule1 % int3)) triple2) -> (rule4 % int2))) -> (rule6 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is not smart.
False
5
inv-proof
[(((((((triple5) -> rule1) triple2) -> rule4)) -> rule6))]
("Bob" "is" "smart" "-")
((((((triple5) -> (rule1 % int3)) triple2) -> (rule4 % int2))) -> (rule6 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Anne is not smart.
Unknown
inv-rconc
[@2: Anne is smart.[CWA. Example of deepest failure = (rule6 <- rule4 <- FAIL)]]
("Anne" "is" "smart" "-")
Anne is big.
Unknown
rconc
[@1: Anne is big.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Anne" "is" "big" "+")
Erin is not blue.
Unknown
inv-random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "-")
Anne is rough.
Unknown
random
[@0: Anne is rough.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "rough" "+")
Erin is not nice.
Unknown
inv-random
[@0: Erin is nice.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "nice" "-")
Anne is blue.
Unknown
random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "+")
Erin is not rough.
Unknown
inv-random
[@0: Erin is rough.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "rough" "-")
Anne is green.
Unknown
random
[@0: Anne is green.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "green" "+")
@0: Anne is white.[(triple1)] Bob is blue.[(triple2)] Bob is green.[(triple3)] Bob is nice.[(triple4)] Bob is rough.[(triple5)] Charlie is big.[(triple6)] Charlie is green.[(triple7)] Charlie is nice.[(triple8)] Charlie is rough.[(triple9 OR ((triple6) -> rule3))] Charlie is smart.[(triple10 OR ((triple6) -> rule6))] Charlie is white.[(triple11 OR ((triple6) -> rule2) OR ((triple9) -> rule1) OR ((((triple6) -> rule3)) -> rule1))] Erin is big.[(triple12)] Erin is green.[(triple13)] Erin is smart.[(triple14 OR ((triple12) -> rule6))] Erin is white.[(triple15 OR ((triple12) -> rule2))] @1: Bob is white.[(((triple5) -> rule1))] @2: Bob is big.[(((((triple5) -> rule1) triple2) -> rule4))] @3: Bob is smart.[(((((((triple5) -> rule1) triple2) -> rule4)) -> rule6))]
Anne is white.
("Anne" "is" "white" "+")
triple1
Bob is blue.
("Bob" "is" "blue" "+")
triple2
Bob is green.
("Bob" "is" "green" "+")
triple3
Bob is nice.
("Bob" "is" "nice" "+")
triple4
Bob is rough.
("Bob" "is" "rough" "+")
triple5
Charlie is big.
("Charlie" "is" "big" "+")
triple6
Charlie is green.
("Charlie" "is" "green" "+")
triple7
Charlie is nice.
("Charlie" "is" "nice" "+")
triple8
Charlie is rough.
("Charlie" "is" "rough" "+")
triple9
((triple6) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
triple10
((triple6) -> (rule6 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
triple11
((triple6) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
((triple9) -> (rule1 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
((((triple6) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
triple12
Erin is green.
("Erin" "is" "green" "+")
triple13
Erin is smart.
("Erin" "is" "smart" "+")
triple14
((triple12) -> (rule6 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
triple15
((triple12) -> (rule2 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
((triple5) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
((((triple5) -> (rule1 % int2)) triple2) -> (rule4 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
((((((triple5) -> (rule1 % int3)) triple2) -> (rule4 % int2))) -> (rule6 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3