Charlie is big. Charlie is cold. Charlie is quiet. Charlie is rough. Charlie is white. Dave is big. Dave is cold. Dave is nice. Dave is rough. Dave is young. Fiona is big. Fiona is cold. Fiona is rough. Fiona is white. Harry is big. Harry is cold. If someone is young then they are nice. If someone is nice then they are quiet. If someone is nice and cold then they are young. All young people are cold. If Harry is big then Harry is nice. If someone is cold and quiet then they are big.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is young.
("Dave" "is" "young" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is cold.
("Harry" "is" "cold" "+")
If someone is young then they are nice.
((("someone" "is" "young" "+")) -> ("someone" "is" "nice" "+"))
If someone is nice then they are quiet.
((("someone" "is" "nice" "+")) -> ("someone" "is" "quiet" "+"))
If someone is nice and cold then they are young.
((("someone" "is" "nice" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "young" "+"))
All young people are cold.
((("someone" "is" "young" "+")) -> ("someone" "is" "cold" "+"))
If Harry is big then Harry is nice.
((("Harry" "is" "big" "+")) -> ("Harry" "is" "nice" "+"))
If someone is cold and quiet then they are big.
((("someone" "is" "cold" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "big" "+"))
Charlie is white.
True
1
proof
[(triple5)]
("Charlie" "is" "white" "+")
triple5
Fiona is not white.
False
1
inv-proof
[(triple14)]
("Fiona" "is" "white" "-")
triple14
Harry is nice.
True
2
proof
[(((triple15) -> rule5))]
("Harry" "is" "nice" "+")
((triple15) -> (rule5 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Dave is not quiet.
False
2
inv-proof
[(((triple8) -> rule2) OR ((((triple10) -> rule1)) -> rule2))]
("Dave" "is" "quiet" "-")
((triple8) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
((((triple10) -> (rule1 % int2))) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Harry is quiet.
True
3
proof
[(((((triple15) -> rule5)) -> rule2))]
("Harry" "is" "quiet" "+")
((((triple15) -> (rule5 % int2))) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is not quiet.
False
3
inv-proof
[(((((triple15) -> rule5)) -> rule2))]
("Harry" "is" "quiet" "-")
((((triple15) -> (rule5 % int2))) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Charlie is not nice.
Unknown
inv-rconc
[@2: Charlie is nice.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("Charlie" "is" "nice" "-")
Fiona is quiet.
Unknown
rconc
[@3: Fiona is quiet.[CWA. Example of deepest failure = (rule2 <- rule1 <- rule3 <- FAIL)]]
("Fiona" "is" "quiet" "+")
Charlie is not young.
Unknown
inv-rconc
[@2: Charlie is young.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("Charlie" "is" "young" "-")
Dave is white.
Unknown
random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "+")
Harry is not rough.
Unknown
inv-random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "-")
Harry is white.
Unknown
random
[@0: Harry is white.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "white" "+")
@0: Charlie is big.[(triple1 OR ((triple2 triple3) -> rule6))] Charlie is cold.[(triple2)] Charlie is quiet.[(triple3)] Charlie is rough.[(triple4)] Charlie is white.[(triple5)] Dave is big.[(triple6 OR ((triple7 ((triple8) -> rule2)) -> rule6) OR ((((triple10) -> rule4) ((triple8) -> rule2)) -> rule6) OR ((triple7 ((((triple10) -> rule1)) -> rule2)) -> rule6) OR ((((triple10) -> rule4) ((((triple10) -> rule1)) -> rule2)) -> rule6))] Dave is cold.[(triple7 OR ((triple10) -> rule4))] Dave is nice.[(triple8 OR ((triple10) -> rule1))] Dave is rough.[(triple9)] Dave is young.[(triple10 OR ((triple8 triple7) -> rule3))] Fiona is big.[(triple11)] Fiona is cold.[(triple12)] Fiona is rough.[(triple13)] Fiona is white.[(triple14)] Harry is big.[(triple15)] Harry is cold.[(triple16)] @1: Dave is quiet.[(((triple8) -> rule2) OR ((((triple10) -> rule1)) -> rule2))] Harry is nice.[(((triple15) -> rule5))] @2: Harry is quiet.[(((((triple15) -> rule5)) -> rule2))] Harry is young.[(((((triple15) -> rule5) triple16) -> rule3))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
((triple2 triple3) -> (rule6 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple3
Charlie is rough.
("Charlie" "is" "rough" "+")
triple4
Charlie is white.
("Charlie" "is" "white" "+")
triple5
Dave is big.
("Dave" "is" "big" "+")
triple6
((triple7 ((triple8) -> (rule2 % int2))) -> (rule6 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
((((triple10) -> (rule4 % int3)) ((triple8) -> (rule2 % int2))) -> (rule6 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
((triple7 ((((triple10) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
((((triple10) -> (rule4 % int4)) ((((triple10) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is cold.
("Dave" "is" "cold" "+")
int4
Dave is cold.
("Dave" "is" "cold" "+")
triple7
((triple10) -> (rule4 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
triple8
((triple10) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
triple9
Dave is young.
("Dave" "is" "young" "+")
triple10
((triple8 triple7) -> (rule3 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
triple11
Fiona is cold.
("Fiona" "is" "cold" "+")
triple12
Fiona is rough.
("Fiona" "is" "rough" "+")
triple13
Fiona is white.
("Fiona" "is" "white" "+")
triple14
Harry is big.
("Harry" "is" "big" "+")
triple15
Harry is cold.
("Harry" "is" "cold" "+")
triple16
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple8) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
((((triple10) -> (rule1 % int2))) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
((triple15) -> (rule5 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
((((triple15) -> (rule5 % int2))) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
((((triple15) -> (rule5 % int2)) triple16) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2