Anne is green. Anne is red. Bob is blue. Bob is quiet. Bob is red. Bob is smart. Fiona is not big. Fiona is green. Fiona is not quiet. Harry is rough. If something is smart then it is quiet. All green, red things are quiet. Green, blue things are red. All rough things are blue. All rough things are not big. Smart, red things are big. If something is quiet and not smart then it is big. If something is quiet and green then it is rough.
Anne is green.
("Anne" "is" "green" "+")
Anne is red.
("Anne" "is" "red" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Fiona is not big.
("Fiona" "is" "big" "-")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is not quiet.
("Fiona" "is" "quiet" "-")
Harry is rough.
("Harry" "is" "rough" "+")
If something is smart then it is quiet.
((("something" "is" "smart" "+")) -> ("something" "is" "quiet" "+"))
All green, red things are quiet.
((("something" "is" "green" "+") ("something" "is" "red" "+")) -> ("something" "is" "quiet" "+"))
Green, blue things are red.
((("something" "is" "green" "+") ("something" "is" "blue" "+")) -> ("something" "is" "red" "+"))
All rough things are blue.
((("something" "is" "rough" "+")) -> ("something" "is" "blue" "+"))
All rough things are not big.
((("something" "is" "rough" "+")) -> ("something" "is" "big" "-"))
Smart, red things are big.
((("something" "is" "smart" "+") ("something" "is" "red" "+")) -> ("something" "is" "big" "+"))
If something is quiet and not smart then it is big.
((("something" "is" "quiet" "+") ("something" "is" "smart" "~")) -> ("something" "is" "big" "+"))
If something is quiet and green then it is rough.
((("something" "is" "quiet" "+") ("something" "is" "green" "+")) -> ("something" "is" "rough" "+"))
Fiona is not big.
True
1
proof
[(triple7)]
("Fiona" "is" "big" "-")
triple7
Bob is not blue.
False
1
inv-proof
[(triple3)]
("Bob" "is" "blue" "-")
triple3
Anne is quiet.
True
3
proof
[(((triple1 triple2) -> rule2))]
("Anne" "is" "quiet" "+")
((triple1 triple2) -> (rule2 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Harry is big.
False
2
inv-proof
[(((triple10) -> rule5))]
("Harry" "is" "big" "+")
((triple10) -> (rule5 % int1))
Harry is not big.
("Harry" "is" "big" "-")
int1
Anne is rough.
True
5
proof
[(((((triple1 triple2) -> rule2) triple1) -> rule8))]
("Anne" "is" "rough" "+")
((((triple1 triple2) -> (rule2 % int2)) triple1) -> (rule8 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is not rough.
False
5
inv-proof
[(((((triple1 triple2) -> rule2) triple1) -> rule8))]
("Anne" "is" "rough" "-")
((((triple1 triple2) -> (rule2 % int2)) triple1) -> (rule8 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is not big.
True
6
proof
[(((((((triple1 triple2) -> rule2) triple1) -> rule8)) -> rule5))]
("Anne" "is" "big" "-")
((((((triple1 triple2) -> (rule2 % int3)) triple1) -> (rule8 % int2))) -> (rule5 % int1))
Anne is not big.
("Anne" "is" "big" "-")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Anne is big.
False
6
inv-proof
[(((((((triple1 triple2) -> rule2) triple1) -> rule8)) -> rule5))]
("Anne" "is" "big" "+")
((((((triple1 triple2) -> (rule2 % int3)) triple1) -> (rule8 % int2))) -> (rule5 % int1))
Anne is not big.
("Anne" "is" "big" "-")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Fiona is not rough.
Unknown
inv-rconc
[@1: Fiona is rough.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Fiona" "is" "rough" "-")
Bob is rough.
Unknown
rconc
[@1: Bob is rough.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Bob" "is" "rough" "+")
Harry is not red.
Unknown
inv-rconc
[@1: Harry is red.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "red" "-")
Harry is quiet.
Unknown
rconc
[@1: Harry is quiet.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "quiet" "+")
Harry is not smart.
Unknown
inv-random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "-")
Bob is green.
Unknown
random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "+")
Harry is not green.
Unknown
inv-random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "-")
Fiona is smart.
Unknown
random
[@0: Fiona is smart.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "smart" "+")
@0: Anne is green.[(triple1)] Anne is red.[(triple2)] Bob is blue.[(triple3)] Bob is quiet.[(triple4 OR ((triple6) -> rule1))] Bob is red.[(triple5)] Bob is smart.[(triple6)] Fiona is green.[(triple8)] Fiona is not big.[(triple7)] Fiona is not quiet.[(triple9)] Harry is rough.[(triple10)] @1: Anne is quiet.[(((triple1 triple2) -> rule2))] Bob is big.[(((triple6 triple5) -> rule6))] Harry is blue.[(((triple10) -> rule4))] Harry is not big.[(((triple10) -> rule5))] @2: Anne is rough.[(((((triple1 triple2) -> rule2) triple1) -> rule8))] @3: Anne is blue.[(((((((triple1 triple2) -> rule2) triple1) -> rule8)) -> rule4))] Anne is not big.[(((((((triple1 triple2) -> rule2) triple1) -> rule8)) -> rule5))]
Anne is green.
("Anne" "is" "green" "+")
triple1
Anne is red.
("Anne" "is" "red" "+")
triple2
Bob is blue.
("Bob" "is" "blue" "+")
triple3
Bob is quiet.
("Bob" "is" "quiet" "+")
triple4
((triple6) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
triple5
Bob is smart.
("Bob" "is" "smart" "+")
triple6
Fiona is green.
("Fiona" "is" "green" "+")
triple8
Fiona is not big.
("Fiona" "is" "big" "-")
triple7
Fiona is not quiet.
("Fiona" "is" "quiet" "-")
triple9
Harry is rough.
("Harry" "is" "rough" "+")
triple10
Anne is quiet.
("Anne" "is" "quiet" "+")
((triple1 triple2) -> (rule2 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
((triple6 triple5) -> (rule6 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
((triple10) -> (rule4 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is not big.
("Harry" "is" "big" "-")
((triple10) -> (rule5 % int1))
Harry is not big.
("Harry" "is" "big" "-")
int1
Anne is rough.
("Anne" "is" "rough" "+")
((((triple1 triple2) -> (rule2 % int2)) triple1) -> (rule8 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
((((((triple1 triple2) -> (rule2 % int3)) triple1) -> (rule8 % int2))) -> (rule4 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Anne is not big.
("Anne" "is" "big" "-")
((((((triple1 triple2) -> (rule2 % int3)) triple1) -> (rule8 % int2))) -> (rule5 % int1))
Anne is not big.
("Anne" "is" "big" "-")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3