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