Anne is smart. Bob is blue. Bob is green. Bob is nice. Fiona is green. Gary is big. Gary is not smart. Smart, blue things are young. All young, blue things are big. If something is nice and not green then it is kind. If something is big then it is kind. Green things are smart. Smart things are blue.
Anne is smart.
("Anne" "is" "smart" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is not smart.
("Gary" "is" "smart" "-")
Smart, blue things are young.
((("something" "is" "smart" "+") ("something" "is" "blue" "+")) -> ("something" "is" "young" "+"))
All young, blue things are big.
((("something" "is" "young" "+") ("something" "is" "blue" "+")) -> ("something" "is" "big" "+"))
If something is nice and not green then it is kind.
((("something" "is" "nice" "+") ("something" "is" "green" "~")) -> ("something" "is" "kind" "+"))
If something is big then it is kind.
((("something" "is" "big" "+")) -> ("something" "is" "kind" "+"))
Green things are smart.
((("something" "is" "green" "+")) -> ("something" "is" "smart" "+"))
Smart things are blue.
((("something" "is" "smart" "+")) -> ("something" "is" "blue" "+"))
Gary is big.
True
1
proof
[(triple6)]
("Gary" "is" "big" "+")
triple6
Bob is not green.
False
1
inv-proof
[(triple3)]
("Bob" "is" "green" "-")
triple3
Anne is blue.
True
2
proof
[(((triple1) -> rule6))]
("Anne" "is" "blue" "+")
((triple1) -> (rule6 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Bob is not smart.
False
2
inv-proof
[(((triple3) -> rule5))]
("Bob" "is" "smart" "-")
((triple3) -> (rule5 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is young.
True
4
proof
[(((((triple3) -> rule5) triple2) -> rule1) OR ((((triple3) -> rule5) ((((triple3) -> rule5)) -> rule6)) -> rule1))]
("Bob" "is" "young" "+")
((((triple3) -> (rule5 % int2)) triple2) -> (rule1 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
((((triple3) -> (rule5 % int3)) ((((triple3) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Anne is not young.
False
4
inv-proof
[(((triple1 ((triple1) -> rule6)) -> rule1))]
("Anne" "is" "young" "-")
((triple1 ((triple1) -> (rule6 % int2))) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Fiona is young.
True
6
proof
[(((((triple5) -> rule5) ((((triple5) -> rule5)) -> rule6)) -> rule1))]
("Fiona" "is" "young" "+")
((((triple5) -> (rule5 % int3)) ((((triple5) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
Bob is not big.
False
6
inv-proof
[(((((((triple3) -> rule5) triple2) -> rule1) triple2) -> rule2) OR ((((((triple3) -> rule5) triple2) -> rule1) ((((triple3) -> rule5)) -> rule6)) -> rule2) OR ((((((triple3) -> rule5) ((((triple3) -> rule5)) -> rule6)) -> rule1) triple2) -> rule2) OR ((((((triple3) -> rule5) ((((triple3) -> rule5)) -> rule6)) -> rule1) ((((triple3) -> rule5)) -> rule6)) -> rule2))]
("Bob" "is" "big" "-")
((((((triple3) -> (rule5 % int3)) triple2) -> (rule1 % int2)) triple2) -> (rule2 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
((((((triple3) -> (rule5 % int4)) triple2) -> (rule1 % int3)) ((((triple3) -> (rule5 % int4))) -> (rule6 % int2))) -> (rule2 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
int4
((((((triple3) -> (rule5 % int4)) ((((triple3) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule1 % int2)) triple2) -> (rule2 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
int4
((((((triple3) -> (rule5 % int4)) ((((triple3) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule1 % int2)) ((((triple3) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule2 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
int4
Anne is kind.
True
8
proof
[(((((((triple1 ((triple1) -> rule6)) -> rule1) ((triple1) -> rule6)) -> rule2)) -> rule4))]
("Anne" "is" "kind" "+")
((((((triple1 ((triple1) -> (rule6 % int4))) -> (rule1 % int3)) ((triple1) -> (rule6 % int4))) -> (rule2 % int2))) -> (rule4 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is blue.
("Anne" "is" "blue" "+")
int4
Fiona is not big.
False
10
inv-proof
[(((((((triple5) -> rule5) ((((triple5) -> rule5)) -> rule6)) -> rule1) ((((triple5) -> rule5)) -> rule6)) -> rule2))]
("Fiona" "is" "big" "-")
((((((triple5) -> (rule5 % int4)) ((((triple5) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule1 % int2)) ((((triple5) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule2 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
Fiona is smart.
("Fiona" "is" "smart" "+")
int4
Fiona is kind.
True
11
proof
[(((((((((triple5) -> rule5) ((((triple5) -> rule5)) -> rule6)) -> rule1) ((((triple5) -> rule5)) -> rule6)) -> rule2)) -> rule4))]
("Fiona" "is" "kind" "+")
((((((((triple5) -> (rule5 % int5)) ((((triple5) -> (rule5 % int5))) -> (rule6 % int4))) -> (rule1 % int3)) ((((triple5) -> (rule5 % int5))) -> (rule6 % int4))) -> (rule2 % int2))) -> (rule4 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Fiona is blue.
("Fiona" "is" "blue" "+")
int4
Fiona is smart.
("Fiona" "is" "smart" "+")
int5
Fiona is not kind.
False
11
inv-proof
[(((((((((triple5) -> rule5) ((((triple5) -> rule5)) -> rule6)) -> rule1) ((((triple5) -> rule5)) -> rule6)) -> rule2)) -> rule4))]
("Fiona" "is" "kind" "-")
((((((((triple5) -> (rule5 % int5)) ((((triple5) -> (rule5 % int5))) -> (rule6 % int4))) -> (rule1 % int3)) ((((triple5) -> (rule5 % int5))) -> (rule6 % int4))) -> (rule2 % int2))) -> (rule4 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Fiona is blue.
("Fiona" "is" "blue" "+")
int4
Fiona is smart.
("Fiona" "is" "smart" "+")
int5
Gary is not young.
Unknown
inv-rconc
[@1: Gary is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "young" "-")
Gary is blue.
Unknown
rconc
[@1: Gary is blue.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Gary" "is" "blue" "+")
Anne is not green.
Unknown
inv-random
[@0: Anne is green.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "green" "-")
Gary is nice.
Unknown
random
[@0: Gary is nice.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "nice" "+")
Fiona is not nice.
Unknown
inv-random
[@0: Fiona is nice.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "nice" "-")
Anne is nice.
Unknown
random
[@0: Anne is nice.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "nice" "+")
@0: Anne is smart.[(triple1)] Bob is blue.[(triple2 OR ((((triple3) -> rule5)) -> rule6))] Bob is green.[(triple3)] Bob is nice.[(triple4)] Fiona is green.[(triple5)] Gary is big.[(triple6)] Gary is not smart.[(triple7)] @1: Anne is blue.[(((triple1) -> rule6))] Bob is smart.[(((triple3) -> rule5))] Fiona is smart.[(((triple5) -> rule5))] Gary is kind.[(((triple6) -> rule4))] @2: Anne is young.[(((triple1 ((triple1) -> rule6)) -> rule1))] Bob is young.[(((((triple3) -> rule5) triple2) -> rule1) OR ((((triple3) -> rule5) ((((triple3) -> rule5)) -> rule6)) -> rule1))] Fiona is blue.[(((((triple5) -> rule5)) -> rule6))] @3: Anne is big.[(((((triple1 ((triple1) -> rule6)) -> rule1) ((triple1) -> rule6)) -> rule2))] Bob is big.[(((((((triple3) -> rule5) triple2) -> rule1) triple2) -> rule2) OR ((((((triple3) -> rule5) triple2) -> rule1) ((((triple3) -> rule5)) -> rule6)) -> rule2) OR ((((((triple3) -> rule5) ((((triple3) -> rule5)) -> rule6)) -> rule1) triple2) -> rule2) OR ((((((triple3) -> rule5) ((((triple3) -> rule5)) -> rule6)) -> rule1) ((((triple3) -> rule5)) -> rule6)) -> rule2))] Fiona is young.[(((((triple5) -> rule5) ((((triple5) -> rule5)) -> rule6)) -> rule1))] @4: Anne is kind.[(((((((triple1 ((triple1) -> rule6)) -> rule1) ((triple1) -> rule6)) -> rule2)) -> rule4))] Bob is kind.[(((((((((triple3) -> rule5) triple2) -> rule1) triple2) -> rule2)) -> rule4) OR ((((((((triple3) -> rule5) triple2) -> rule1) ((((triple3) -> rule5)) -> rule6)) -> rule2)) -> rule4) OR ((((((((triple3) -> rule5) ((((triple3) -> rule5)) -> rule6)) -> rule1) triple2) -> rule2)) -> rule4) OR ((((((((triple3) -> rule5) ((((triple3) -> rule5)) -> rule6)) -> rule1) ((((triple3) -> rule5)) -> rule6)) -> rule2)) -> rule4))] Fiona is big.[(((((((triple5) -> rule5) ((((triple5) -> rule5)) -> rule6)) -> rule1) ((((triple5) -> rule5)) -> rule6)) -> rule2))] @5: Fiona is kind.[(((((((((triple5) -> rule5) ((((triple5) -> rule5)) -> rule6)) -> rule1) ((((triple5) -> rule5)) -> rule6)) -> rule2)) -> rule4))]
Anne is smart.
("Anne" "is" "smart" "+")
triple1
Bob is blue.
("Bob" "is" "blue" "+")
triple2
((((triple3) -> (rule5 % int2))) -> (rule6 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
triple3
Bob is nice.
("Bob" "is" "nice" "+")
triple4
Fiona is green.
("Fiona" "is" "green" "+")
triple5
Gary is big.
("Gary" "is" "big" "+")
triple6
Gary is not smart.
("Gary" "is" "smart" "-")
triple7
Anne is blue.
("Anne" "is" "blue" "+")
((triple1) -> (rule6 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
((triple3) -> (rule5 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
((triple5) -> (rule5 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
((triple6) -> (rule4 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
((triple1 ((triple1) -> (rule6 % int2))) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
((((triple3) -> (rule5 % int2)) triple2) -> (rule1 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
((((triple3) -> (rule5 % int3)) ((((triple3) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Fiona is blue.
("Fiona" "is" "blue" "+")
((((triple5) -> (rule5 % int2))) -> (rule6 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
((((triple1 ((triple1) -> (rule6 % int3))) -> (rule1 % int2)) ((triple1) -> (rule6 % int3))) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
Bob is big.
("Bob" "is" "big" "+")
((((((triple3) -> (rule5 % int3)) triple2) -> (rule1 % int2)) triple2) -> (rule2 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
((((((triple3) -> (rule5 % int4)) triple2) -> (rule1 % int3)) ((((triple3) -> (rule5 % int4))) -> (rule6 % int2))) -> (rule2 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
int4
((((((triple3) -> (rule5 % int4)) ((((triple3) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule1 % int2)) triple2) -> (rule2 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
int4
((((((triple3) -> (rule5 % int4)) ((((triple3) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule1 % int2)) ((((triple3) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule2 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
int4
Fiona is young.
("Fiona" "is" "young" "+")
((((triple5) -> (rule5 % int3)) ((((triple5) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
Anne is kind.
("Anne" "is" "kind" "+")
((((((triple1 ((triple1) -> (rule6 % int4))) -> (rule1 % int3)) ((triple1) -> (rule6 % int4))) -> (rule2 % int2))) -> (rule4 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is blue.
("Anne" "is" "blue" "+")
int4
Bob is kind.
("Bob" "is" "kind" "+")
((((((((triple3) -> (rule5 % int4)) triple2) -> (rule1 % int3)) triple2) -> (rule2 % int2))) -> (rule4 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
int4
((((((((triple3) -> (rule5 % int5)) triple2) -> (rule1 % int4)) ((((triple3) -> (rule5 % int5))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Bob is young.
("Bob" "is" "young" "+")
int4
Bob is smart.
("Bob" "is" "smart" "+")
int5
((((((((triple3) -> (rule5 % int5)) ((((triple3) -> (rule5 % int5))) -> (rule6 % int4))) -> (rule1 % int3)) triple2) -> (rule2 % int2))) -> (rule4 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is blue.
("Bob" "is" "blue" "+")
int4
Bob is smart.
("Bob" "is" "smart" "+")
int5
((((((((triple3) -> (rule5 % int5)) ((((triple3) -> (rule5 % int5))) -> (rule6 % int4))) -> (rule1 % int3)) ((((triple3) -> (rule5 % int5))) -> (rule6 % int4))) -> (rule2 % int2))) -> (rule4 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is blue.
("Bob" "is" "blue" "+")
int4
Bob is smart.
("Bob" "is" "smart" "+")
int5
Fiona is big.
("Fiona" "is" "big" "+")
((((((triple5) -> (rule5 % int4)) ((((triple5) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule1 % int2)) ((((triple5) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule2 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
Fiona is smart.
("Fiona" "is" "smart" "+")
int4
Fiona is kind.
("Fiona" "is" "kind" "+")
((((((((triple5) -> (rule5 % int5)) ((((triple5) -> (rule5 % int5))) -> (rule6 % int4))) -> (rule1 % int3)) ((((triple5) -> (rule5 % int5))) -> (rule6 % int4))) -> (rule2 % int2))) -> (rule4 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Fiona is blue.
("Fiona" "is" "blue" "+")
int4
Fiona is smart.
("Fiona" "is" "smart" "+")
int5