Anne is big. Anne is nice. Anne is round. Fiona is nice. Fiona is round. Fiona is not young. Gary is blue. If someone is young then they are blue. All green people are blue. If someone is green then they are nice. Blue, young people are green. If someone is big then they are young. If someone is nice then they are round.
Anne is big.
("Anne" "is" "big" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is round.
("Anne" "is" "round" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Fiona is not young.
("Fiona" "is" "young" "-")
Gary is blue.
("Gary" "is" "blue" "+")
If someone is young then they are blue.
((("someone" "is" "young" "+")) -> ("someone" "is" "blue" "+"))
All green people are blue.
((("someone" "is" "green" "+")) -> ("someone" "is" "blue" "+"))
If someone is green then they are nice.
((("someone" "is" "green" "+")) -> ("someone" "is" "nice" "+"))
Blue, young people are green.
((("someone" "is" "blue" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "green" "+"))
If someone is big then they are young.
((("someone" "is" "big" "+")) -> ("someone" "is" "young" "+"))
If someone is nice then they are round.
((("someone" "is" "nice" "+")) -> ("someone" "is" "round" "+"))
Anne is round.
True
1
proof
[(triple3 OR ((triple2) -> rule6) OR ((((((((((triple1) -> rule5)) -> rule1) ((triple1) -> rule5)) -> rule4)) -> rule3)) -> rule6))]
("Anne" "is" "round" "+")
triple3
((triple2) -> (rule6 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
((((((((((triple1) -> (rule5 % int5))) -> (rule1 % int4)) ((triple1) -> (rule5 % int5))) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is blue.
("Anne" "is" "blue" "+")
int4
Anne is young.
("Anne" "is" "young" "+")
int5
Anne is not round.
False
1
inv-proof
[(triple3 OR ((triple2) -> rule6) OR ((((((((((triple1) -> rule5)) -> rule1) ((triple1) -> rule5)) -> rule4)) -> rule3)) -> rule6))]
("Anne" "is" "round" "-")
triple3
((triple2) -> (rule6 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
((((((((((triple1) -> (rule5 % int5))) -> (rule1 % int4)) ((triple1) -> (rule5 % int5))) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is blue.
("Anne" "is" "blue" "+")
int4
Anne is young.
("Anne" "is" "young" "+")
int5
Anne is young.
True
2
proof
[(((triple1) -> rule5))]
("Anne" "is" "young" "+")
((triple1) -> (rule5 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is not young.
False
2
inv-proof
[(((triple1) -> rule5))]
("Anne" "is" "young" "-")
((triple1) -> (rule5 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is blue.
True
3
proof
[(((((triple1) -> rule5)) -> rule1))]
("Anne" "is" "blue" "+")
((((triple1) -> (rule5 % int2))) -> (rule1 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is not blue.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule1))]
("Anne" "is" "blue" "-")
((((triple1) -> (rule5 % int2))) -> (rule1 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is green.
True
6
proof
[(((((((triple1) -> rule5)) -> rule1) ((triple1) -> rule5)) -> rule4))]
("Anne" "is" "green" "+")
((((((triple1) -> (rule5 % int3))) -> (rule1 % int2)) ((triple1) -> (rule5 % int3))) -> (rule4 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is not green.
False
6
inv-proof
[(((((((triple1) -> rule5)) -> rule1) ((triple1) -> rule5)) -> rule4))]
("Anne" "is" "green" "-")
((((((triple1) -> (rule5 % int3))) -> (rule1 % int2)) ((triple1) -> (rule5 % int3))) -> (rule4 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Fiona is not green.
Unknown
inv-rconc
[@1: Fiona is green.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Fiona" "is" "green" "-")
Fiona is blue.
Unknown
rconc
[@2: Fiona is blue.[CWA. Example of deepest failure = (rule2 <- rule4 <- FAIL)]]
("Fiona" "is" "blue" "+")
Gary is not round.
Unknown
inv-rconc
[@4: Gary is round.[CWA. Example of deepest failure = (rule6 <- rule3 <- rule4 <- rule5 <- FAIL)]]
("Gary" "is" "round" "-")
Gary is green.
Unknown
rconc
[@2: Gary is green.[CWA. Example of deepest failure = (rule4 <- rule5 <- FAIL)]]
("Gary" "is" "green" "+")
Gary is not white.
Unknown
inv-random
[@0: Gary is white.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "white" "-")
Fiona is big.
Unknown
random
[@0: Fiona is big.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "big" "+")
Gary is not big.
Unknown
inv-random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "-")
Fiona is white.
Unknown
random
[@0: Fiona is white.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "white" "+")
@0: Anne is big.[(triple1)] Anne is nice.[(triple2 OR ((((((((triple1) -> rule5)) -> rule1) ((triple1) -> rule5)) -> rule4)) -> rule3))] Anne is round.[(triple3 OR ((triple2) -> rule6) OR ((((((((((triple1) -> rule5)) -> rule1) ((triple1) -> rule5)) -> rule4)) -> rule3)) -> rule6))] Fiona is nice.[(triple4)] Fiona is not young.[(triple6)] Fiona is round.[(triple5 OR ((triple4) -> rule6))] Gary is blue.[(triple7)] @1: Anne is young.[(((triple1) -> rule5))] @2: Anne is blue.[(((((triple1) -> rule5)) -> rule1))] @3: Anne is green.[(((((((triple1) -> rule5)) -> rule1) ((triple1) -> rule5)) -> rule4))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is nice.
("Anne" "is" "nice" "+")
triple2
((((((((triple1) -> (rule5 % int4))) -> (rule1 % int3)) ((triple1) -> (rule5 % int4))) -> (rule4 % int2))) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
Anne is young.
("Anne" "is" "young" "+")
int4
Anne is round.
("Anne" "is" "round" "+")
triple3
((triple2) -> (rule6 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
((((((((((triple1) -> (rule5 % int5))) -> (rule1 % int4)) ((triple1) -> (rule5 % int5))) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is blue.
("Anne" "is" "blue" "+")
int4
Anne is young.
("Anne" "is" "young" "+")
int5
Fiona is nice.
("Fiona" "is" "nice" "+")
triple4
Fiona is not young.
("Fiona" "is" "young" "-")
triple6
Fiona is round.
("Fiona" "is" "round" "+")
triple5
((triple4) -> (rule6 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
triple7
Anne is young.
("Anne" "is" "young" "+")
((triple1) -> (rule5 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
((((triple1) -> (rule5 % int2))) -> (rule1 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
((((((triple1) -> (rule5 % int3))) -> (rule1 % int2)) ((triple1) -> (rule5 % int3))) -> (rule4 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3