Anne is quiet. Anne is smart. Fiona is big. If something is smart and big then it is rough. All big things are quiet. If something is cold and young then it is blue. If something is blue then it is smart. If something is big and rough then it is young. If something is cold and young then it is rough. If Anne is smart and Anne is big then Anne is blue. If something is quiet then it is blue.
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Fiona is big.
("Fiona" "is" "big" "+")
If something is smart and big then it is rough.
((("something" "is" "smart" "+") ("something" "is" "big" "+")) -> ("something" "is" "rough" "+"))
All big things are quiet.
((("something" "is" "big" "+")) -> ("something" "is" "quiet" "+"))
If something is cold and young then it is blue.
((("something" "is" "cold" "+") ("something" "is" "young" "+")) -> ("something" "is" "blue" "+"))
If something is blue then it is smart.
((("something" "is" "blue" "+")) -> ("something" "is" "smart" "+"))
If something is big and rough then it is young.
((("something" "is" "big" "+") ("something" "is" "rough" "+")) -> ("something" "is" "young" "+"))
If something is cold and young then it is rough.
((("something" "is" "cold" "+") ("something" "is" "young" "+")) -> ("something" "is" "rough" "+"))
If Anne is smart and Anne is big then Anne is blue.
((("Anne" "is" "smart" "+") ("Anne" "is" "big" "+")) -> ("Anne" "is" "blue" "+"))
If something is quiet then it is blue.
((("something" "is" "quiet" "+")) -> ("something" "is" "blue" "+"))
Fiona is big.
True
1
proof
[(triple3)]
("Fiona" "is" "big" "+")
triple3
Anne is not smart.
False
1
inv-proof
[(triple2 OR ((((triple1) -> rule8)) -> rule4))]
("Anne" "is" "smart" "-")
triple2
((((triple1) -> (rule8 % int2))) -> (rule4 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is blue.
True
2
proof
[(((triple1) -> rule8))]
("Anne" "is" "blue" "+")
((triple1) -> (rule8 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Fiona is not quiet.
False
2
inv-proof
[(((triple3) -> rule2))]
("Fiona" "is" "quiet" "-")
((triple3) -> (rule2 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is blue.
True
3
proof
[(((((triple3) -> rule2)) -> rule8))]
("Fiona" "is" "blue" "+")
((((triple3) -> (rule2 % int2))) -> (rule8 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is not blue.
False
3
inv-proof
[(((((triple3) -> rule2)) -> rule8))]
("Fiona" "is" "blue" "-")
((((triple3) -> (rule2 % int2))) -> (rule8 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Anne is not rough.
Unknown
inv-rconc
[@1: Anne is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "rough" "-")
Anne is young.
Unknown
rconc
[@1: Anne is young.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Anne" "is" "young" "+")
Anne is not big.
Unknown
inv-random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "-")
Fiona is cold.
Unknown
random
[@0: Fiona is cold.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "cold" "+")
@0: Anne is quiet.[(triple1)] Anne is smart.[(triple2 OR ((((triple1) -> rule8)) -> rule4))] Fiona is big.[(triple3)] @1: Anne is blue.[(((triple1) -> rule8))] Fiona is quiet.[(((triple3) -> rule2))] @2: Fiona is blue.[(((((triple3) -> rule2)) -> rule8))] @3: Fiona is smart.[(((((((triple3) -> rule2)) -> rule8)) -> rule4))] @4: Fiona is rough.[(((((((((triple3) -> rule2)) -> rule8)) -> rule4) triple3) -> rule1))] @5: Fiona is young.[(((triple3 ((((((((triple3) -> rule2)) -> rule8)) -> rule4) triple3) -> rule1)) -> rule5))]
Anne is quiet.
("Anne" "is" "quiet" "+")
triple1
Anne is smart.
("Anne" "is" "smart" "+")
triple2
((((triple1) -> (rule8 % int2))) -> (rule4 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
triple3
Anne is blue.
("Anne" "is" "blue" "+")
((triple1) -> (rule8 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((triple3) -> (rule2 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
((((triple3) -> (rule2 % int2))) -> (rule8 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
((((((triple3) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
Fiona is rough.
("Fiona" "is" "rough" "+")
((((((((triple3) -> (rule2 % int4))) -> (rule8 % int3))) -> (rule4 % int2)) triple3) -> (rule1 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int4
Fiona is young.
("Fiona" "is" "young" "+")
((triple3 ((((((((triple3) -> (rule2 % int5))) -> (rule8 % int4))) -> (rule4 % int3)) triple3) -> (rule1 % int2))) -> (rule5 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
Fiona is blue.
("Fiona" "is" "blue" "+")
int4
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int5