Anne is nice. Anne is rough. Anne is young. Charlie is kind. Charlie is nice. Fiona is nice. Fiona is quiet. Fiona is smart. Fiona is young. Gary is big. Gary is kind. Gary is rough. All young people are kind. If someone is young and smart then they are quiet. If Anne is smart and Anne is kind then Anne is rough. Rough, smart people are young. If someone is quiet then they are big. Kind people are big. If Anne is rough then Anne is smart. All smart people are rough.
Anne is nice.
("Anne" "is" "nice" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is young.
("Anne" "is" "young" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Fiona is young.
("Fiona" "is" "young" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is rough.
("Gary" "is" "rough" "+")
All young people are kind.
((("someone" "is" "young" "+")) -> ("someone" "is" "kind" "+"))
If someone is young and smart then they are quiet.
((("someone" "is" "young" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "quiet" "+"))
If Anne is smart and Anne is kind then Anne is rough.
((("Anne" "is" "smart" "+") ("Anne" "is" "kind" "+")) -> ("Anne" "is" "rough" "+"))
Rough, smart people are young.
((("someone" "is" "rough" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "young" "+"))
If someone is quiet then they are big.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "big" "+"))
Kind people are big.
((("someone" "is" "kind" "+")) -> ("someone" "is" "big" "+"))
If Anne is rough then Anne is smart.
((("Anne" "is" "rough" "+")) -> ("Anne" "is" "smart" "+"))
All smart people are rough.
((("someone" "is" "smart" "+")) -> ("someone" "is" "rough" "+"))
Fiona is smart.
True
1
proof
[(triple8)]
("Fiona" "is" "smart" "+")
triple8
Anne is not young.
False
1
inv-proof
[(triple3 OR ((triple2 ((triple2) -> rule7)) -> rule4))]
("Anne" "is" "young" "-")
triple3
((triple2 ((triple2) -> (rule7 % int2))) -> (rule4 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is kind.
True
2
proof
[(((triple3) -> rule1) OR ((((triple2 ((triple2) -> rule7)) -> rule4)) -> rule1))]
("Anne" "is" "kind" "+")
((triple3) -> (rule1 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
((((triple2 ((triple2) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is not smart.
False
2
inv-proof
[(((triple2) -> rule7))]
("Anne" "is" "smart" "-")
((triple2) -> (rule7 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Gary is not quiet.
Unknown
inv-rconc
[@1: Gary is quiet.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "quiet" "-")
Charlie is quiet.
Unknown
rconc
[@1: Charlie is quiet.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "quiet" "+")
Gary is not smart.
Unknown
inv-random
[@0: Gary is smart.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "smart" "-")
Gary is nice.
Unknown
random
[@0: Gary is nice.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "nice" "+")
@0: Anne is nice.[(triple1)] Anne is rough.[(triple2)] Anne is young.[(triple3 OR ((triple2 ((triple2) -> rule7)) -> rule4))] Charlie is kind.[(triple4)] Charlie is nice.[(triple5)] Fiona is nice.[(triple6)] Fiona is quiet.[(triple7 OR ((triple9 triple8) -> rule2) OR ((((((triple8) -> rule8) triple8) -> rule4) triple8) -> rule2))] Fiona is smart.[(triple8)] Fiona is young.[(triple9 OR ((((triple8) -> rule8) triple8) -> rule4))] Gary is big.[(triple10 OR ((triple11) -> rule6))] Gary is kind.[(triple11)] Gary is rough.[(triple12)] @1: Anne is kind.[(((triple3) -> rule1) OR ((((triple2 ((triple2) -> rule7)) -> rule4)) -> rule1))] Anne is smart.[(((triple2) -> rule7))] Charlie is big.[(((triple4) -> rule6))] Fiona is big.[(((triple7) -> rule5) OR ((((triple9) -> rule1)) -> rule6) OR ((((triple9 triple8) -> rule2)) -> rule5) OR ((((((((triple8) -> rule8) triple8) -> rule4)) -> rule1)) -> rule6) OR ((((((((triple8) -> rule8) triple8) -> rule4) triple8) -> rule2)) -> rule5))] Fiona is kind.[(((triple9) -> rule1) OR ((((((triple8) -> rule8) triple8) -> rule4)) -> rule1))] Fiona is rough.[(((triple8) -> rule8))] @2: Anne is big.[(((((triple3) -> rule1)) -> rule6) OR ((((triple3 ((triple2) -> rule7)) -> rule2)) -> rule5) OR ((((((triple2 ((triple2) -> rule7)) -> rule4)) -> rule1)) -> rule6) OR ((((((triple2 ((triple2) -> rule7)) -> rule4) ((triple2) -> rule7)) -> rule2)) -> rule5))] Anne is quiet.[(((triple3 ((triple2) -> rule7)) -> rule2) OR ((((triple2 ((triple2) -> rule7)) -> rule4) ((triple2) -> rule7)) -> rule2))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Anne is rough.
("Anne" "is" "rough" "+")
triple2
Anne is young.
("Anne" "is" "young" "+")
triple3
((triple2 ((triple2) -> (rule7 % int2))) -> (rule4 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
triple4
Charlie is nice.
("Charlie" "is" "nice" "+")
triple5
Fiona is nice.
("Fiona" "is" "nice" "+")
triple6
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple7
((triple9 triple8) -> (rule2 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
((((((triple8) -> (rule8 % int3)) triple8) -> (rule4 % int2)) triple8) -> (rule2 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
int3
Fiona is smart.
("Fiona" "is" "smart" "+")
triple8
Fiona is young.
("Fiona" "is" "young" "+")
triple9
((((triple8) -> (rule8 % int2)) triple8) -> (rule4 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
triple10
((triple11) -> (rule6 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
triple11
Gary is rough.
("Gary" "is" "rough" "+")
triple12
Anne is kind.
("Anne" "is" "kind" "+")
((triple3) -> (rule1 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
((((triple2 ((triple2) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
((triple2) -> (rule7 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
((triple4) -> (rule6 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
((triple7) -> (rule5 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
((((triple9) -> (rule1 % int2))) -> (rule6 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
((((triple9 triple8) -> (rule2 % int2))) -> (rule5 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
((((((((triple8) -> (rule8 % int4)) triple8) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Fiona is rough.
("Fiona" "is" "rough" "+")
int4
((((((((triple8) -> (rule8 % int4)) triple8) -> (rule4 % int3)) triple8) -> (rule2 % int2))) -> (rule5 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Fiona is rough.
("Fiona" "is" "rough" "+")
int4
Fiona is kind.
("Fiona" "is" "kind" "+")
((triple9) -> (rule1 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
((((((triple8) -> (rule8 % int3)) triple8) -> (rule4 % int2))) -> (rule1 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
int3
Fiona is rough.
("Fiona" "is" "rough" "+")
((triple8) -> (rule8 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
((((triple3) -> (rule1 % int2))) -> (rule6 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
((((triple3 ((triple2) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
((((((triple2 ((triple2) -> (rule7 % int4))) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
int4
((((((triple2 ((triple2) -> (rule7 % int4))) -> (rule4 % int3)) ((triple2) -> (rule7 % int4))) -> (rule2 % int2))) -> (rule5 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
int4
Anne is quiet.
("Anne" "is" "quiet" "+")
((triple3 ((triple2) -> (rule7 % int2))) -> (rule2 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
((((triple2 ((triple2) -> (rule7 % int3))) -> (rule4 % int2)) ((triple2) -> (rule7 % int3))) -> (rule2 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3