Charlie is big. Charlie is nice. Fiona is quiet. Fiona is round. Gary is big. Gary is quiet. Gary is rough. Big things are rough. Big things are quiet. All big, nice things are quiet. If Gary is quiet and Gary is young then Gary is nice. Rough things are red. If Charlie is young and Charlie is quiet then Charlie is big. If something is nice then it is round. If something is rough and big then it is nice.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Big things are rough.
((("something" "is" "big" "+")) -> ("something" "is" "rough" "+"))
Big things are quiet.
((("something" "is" "big" "+")) -> ("something" "is" "quiet" "+"))
All big, nice things are quiet.
((("something" "is" "big" "+") ("something" "is" "nice" "+")) -> ("something" "is" "quiet" "+"))
If Gary is quiet and Gary is young then Gary is nice.
((("Gary" "is" "quiet" "+") ("Gary" "is" "young" "+")) -> ("Gary" "is" "nice" "+"))
Rough things are red.
((("something" "is" "rough" "+")) -> ("something" "is" "red" "+"))
If Charlie is young and Charlie is quiet then Charlie is big.
((("Charlie" "is" "young" "+") ("Charlie" "is" "quiet" "+")) -> ("Charlie" "is" "big" "+"))
If something is nice then it is round.
((("something" "is" "nice" "+")) -> ("something" "is" "round" "+"))
If something is rough and big then it is nice.
((("something" "is" "rough" "+") ("something" "is" "big" "+")) -> ("something" "is" "nice" "+"))
Fiona is quiet.
True
1
proof
[(triple3)]
("Fiona" "is" "quiet" "+")
triple3
Gary is not quiet.
False
1
inv-proof
[(triple6 OR ((triple5) -> rule2) OR ((triple5 ((triple7 triple5) -> rule8)) -> rule3) OR ((triple5 ((((triple5) -> rule1) triple5) -> rule8)) -> rule3))]
("Gary" "is" "quiet" "-")
triple6
((triple5) -> (rule2 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
((triple5 ((triple7 triple5) -> (rule8 % int2))) -> (rule3 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
((triple5 ((((triple5) -> (rule1 % int3)) triple5) -> (rule8 % int2))) -> (rule3 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Fiona is not rough.
Unknown
inv-rconc
[@1: Fiona is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "rough" "-")
Gary is young.
Unknown
random
[@0: Gary is young.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "young" "+")
@0: Charlie is big.[(triple1)] Charlie is nice.[(triple2 OR ((((triple1) -> rule1) triple1) -> rule8))] Fiona is quiet.[(triple3)] Fiona is round.[(triple4)] Gary is big.[(triple5)] Gary is quiet.[(triple6 OR ((triple5) -> rule2) OR ((triple5 ((triple7 triple5) -> rule8)) -> rule3) OR ((triple5 ((((triple5) -> rule1) triple5) -> rule8)) -> rule3))] Gary is rough.[(triple7 OR ((triple5) -> rule1))] @1: Charlie is quiet.[(((triple1) -> rule2) OR ((triple1 triple2) -> rule3) OR ((triple1 ((((triple1) -> rule1) triple1) -> rule8)) -> rule3))] Charlie is rough.[(((triple1) -> rule1))] Charlie is round.[(((triple2) -> rule7) OR ((((((triple1) -> rule1) triple1) -> rule8)) -> rule7))] Gary is nice.[(((triple7 triple5) -> rule8) OR ((((triple5) -> rule1) triple5) -> rule8))] Gary is red.[(((triple7) -> rule5) OR ((((triple5) -> rule1)) -> rule5))] @2: Charlie is red.[(((((triple1) -> rule1)) -> rule5))] Gary is round.[(((((triple7 triple5) -> rule8)) -> rule7) OR ((((((triple5) -> rule1) triple5) -> rule8)) -> rule7))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Charlie is nice.
("Charlie" "is" "nice" "+")
triple2
((((triple1) -> (rule1 % int2)) triple1) -> (rule8 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple3
Fiona is round.
("Fiona" "is" "round" "+")
triple4
Gary is big.
("Gary" "is" "big" "+")
triple5
Gary is quiet.
("Gary" "is" "quiet" "+")
triple6
((triple5) -> (rule2 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
((triple5 ((triple7 triple5) -> (rule8 % int2))) -> (rule3 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
((triple5 ((((triple5) -> (rule1 % int3)) triple5) -> (rule8 % int2))) -> (rule3 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Gary is rough.
("Gary" "is" "rough" "+")
triple7
((triple5) -> (rule1 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple1) -> (rule2 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
((triple1 triple2) -> (rule3 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
((triple1 ((((triple1) -> (rule1 % int3)) triple1) -> (rule8 % int2))) -> (rule3 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple1) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
((triple2) -> (rule7 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
((((((triple1) -> (rule1 % int3)) triple1) -> (rule8 % int2))) -> (rule7 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Gary is nice.
("Gary" "is" "nice" "+")
((triple7 triple5) -> (rule8 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
((((triple5) -> (rule1 % int2)) triple5) -> (rule8 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
((triple7) -> (rule5 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
((((triple5) -> (rule1 % int2))) -> (rule5 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
((((triple1) -> (rule1 % int2))) -> (rule5 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
((((triple7 triple5) -> (rule8 % int2))) -> (rule7 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
((((((triple5) -> (rule1 % int3)) triple5) -> (rule8 % int2))) -> (rule7 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3