Charlie is big. Charlie is furry. Charlie is quiet. Charlie is red. Dave is nice. Dave is quiet. Dave is young. Fiona is nice. Fiona is smart. Harry is big. Harry is quiet. Harry is smart. All smart people are furry. All red people are nice. Smart, furry people are quiet. If Harry is red and Harry is nice then Harry is furry. All nice, young people are red. All red people are big. If Fiona is quiet then Fiona is young. Nice, red people are big.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is young.
("Dave" "is" "young" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is smart.
("Harry" "is" "smart" "+")
All smart people are furry.
((("someone" "is" "smart" "+")) -> ("someone" "is" "furry" "+"))
All red people are nice.
((("someone" "is" "red" "+")) -> ("someone" "is" "nice" "+"))
Smart, furry people are quiet.
((("someone" "is" "smart" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "quiet" "+"))
If Harry is red and Harry is nice then Harry is furry.
((("Harry" "is" "red" "+") ("Harry" "is" "nice" "+")) -> ("Harry" "is" "furry" "+"))
All nice, young people are red.
((("someone" "is" "nice" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "red" "+"))
All red people are big.
((("someone" "is" "red" "+")) -> ("someone" "is" "big" "+"))
If Fiona is quiet then Fiona is young.
((("Fiona" "is" "quiet" "+")) -> ("Fiona" "is" "young" "+"))
Nice, red people are big.
((("someone" "is" "nice" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "big" "+"))
Charlie is red.
True
1
proof
[(triple4)]
("Charlie" "is" "red" "+")
triple4
Fiona is not nice.
False
1
inv-proof
[(triple8)]
("Fiona" "is" "nice" "-")
triple8
Harry is furry.
True
2
proof
[(((triple12) -> rule1))]
("Harry" "is" "furry" "+")
((triple12) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Charlie is not nice.
False
2
inv-proof
[(((triple4) -> rule2))]
("Charlie" "is" "nice" "-")
((triple4) -> (rule2 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Fiona is quiet.
True
4
proof
[(((triple9 ((triple9) -> rule1)) -> rule3))]
("Fiona" "is" "quiet" "+")
((triple9 ((triple9) -> (rule1 % int2))) -> (rule3 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
Dave is not big.
False
4
inv-proof
[(((((triple5 triple7) -> rule5)) -> rule6) OR ((triple5 ((triple5 triple7) -> rule5)) -> rule8))]
("Dave" "is" "big" "-")
((((triple5 triple7) -> (rule5 % int2))) -> (rule6 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
((triple5 ((triple5 triple7) -> (rule5 % int2))) -> (rule8 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Fiona is young.
True
5
proof
[(((((triple9 ((triple9) -> rule1)) -> rule3)) -> rule7))]
("Fiona" "is" "young" "+")
((((triple9 ((triple9) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
int3
Fiona is not young.
False
5
inv-proof
[(((((triple9 ((triple9) -> rule1)) -> rule3)) -> rule7))]
("Fiona" "is" "young" "-")
((((triple9 ((triple9) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
int3
Fiona is red.
True
7
proof
[(((triple8 ((((triple9 ((triple9) -> rule1)) -> rule3)) -> rule7)) -> rule5))]
("Fiona" "is" "red" "+")
((triple8 ((((triple9 ((triple9) -> (rule1 % int4))) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
Fiona is furry.
("Fiona" "is" "furry" "+")
int4
Fiona is not red.
False
7
inv-proof
[(((triple8 ((((triple9 ((triple9) -> rule1)) -> rule3)) -> rule7)) -> rule5))]
("Fiona" "is" "red" "-")
((triple8 ((((triple9 ((triple9) -> (rule1 % int4))) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
Fiona is furry.
("Fiona" "is" "furry" "+")
int4
Fiona is big.
True
8
proof
[(((((triple8 ((((triple9 ((triple9) -> rule1)) -> rule3)) -> rule7)) -> rule5)) -> rule6) OR ((triple8 ((triple8 ((((triple9 ((triple9) -> rule1)) -> rule3)) -> rule7)) -> rule5)) -> rule8))]
("Fiona" "is" "big" "+")
((((triple8 ((((triple9 ((triple9) -> (rule1 % int5))) -> (rule3 % int4))) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int4
Fiona is furry.
("Fiona" "is" "furry" "+")
int5
((triple8 ((triple8 ((((triple9 ((triple9) -> (rule1 % int5))) -> (rule3 % int4))) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int4
Fiona is furry.
("Fiona" "is" "furry" "+")
int5
Fiona is not big.
False
8
inv-proof
[(((((triple8 ((((triple9 ((triple9) -> rule1)) -> rule3)) -> rule7)) -> rule5)) -> rule6) OR ((triple8 ((triple8 ((((triple9 ((triple9) -> rule1)) -> rule3)) -> rule7)) -> rule5)) -> rule8))]
("Fiona" "is" "big" "-")
((((triple8 ((((triple9 ((triple9) -> (rule1 % int5))) -> (rule3 % int4))) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int4
Fiona is furry.
("Fiona" "is" "furry" "+")
int5
((triple8 ((triple8 ((((triple9 ((triple9) -> (rule1 % int5))) -> (rule3 % int4))) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int4
Fiona is furry.
("Fiona" "is" "furry" "+")
int5
Harry is not nice.
Unknown
inv-rconc
[@2: Harry is nice.[CWA. Example of deepest failure = (rule2 <- rule5 <- FAIL)]]
("Harry" "is" "nice" "-")
Dave is furry.
Unknown
rconc
[@1: Dave is furry.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "furry" "+")
Harry is not red.
Unknown
inv-rconc
[@1: Harry is red.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Harry" "is" "red" "-")
Dave is smart.
Unknown
random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "+")
Charlie is not smart.
Unknown
inv-random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "-")
Charlie is young.
Unknown
random
[@0: Charlie is young.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "young" "+")
@0: Charlie is big.[(triple1 OR ((triple4) -> rule6) OR ((((triple4) -> rule2) triple4) -> rule8))] Charlie is furry.[(triple2)] Charlie is quiet.[(triple3)] Charlie is red.[(triple4)] Dave is nice.[(triple5)] Dave is quiet.[(triple6)] Dave is young.[(triple7)] Fiona is nice.[(triple8)] Fiona is smart.[(triple9)] Harry is big.[(triple10)] Harry is quiet.[(triple11 OR ((triple12 ((triple12) -> rule1)) -> rule3))] Harry is smart.[(triple12)] @1: Charlie is nice.[(((triple4) -> rule2))] Dave is red.[(((triple5 triple7) -> rule5))] Fiona is furry.[(((triple9) -> rule1))] Harry is furry.[(((triple12) -> rule1))] @2: Dave is big.[(((((triple5 triple7) -> rule5)) -> rule6) OR ((triple5 ((triple5 triple7) -> rule5)) -> rule8))] Fiona is quiet.[(((triple9 ((triple9) -> rule1)) -> rule3))] @3: Fiona is young.[(((((triple9 ((triple9) -> rule1)) -> rule3)) -> rule7))] @4: Fiona is red.[(((triple8 ((((triple9 ((triple9) -> rule1)) -> rule3)) -> rule7)) -> rule5))] @5: Fiona is big.[(((((triple8 ((((triple9 ((triple9) -> rule1)) -> rule3)) -> rule7)) -> rule5)) -> rule6) OR ((triple8 ((triple8 ((((triple9 ((triple9) -> rule1)) -> rule3)) -> rule7)) -> rule5)) -> rule8))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
((triple4) -> (rule6 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
((((triple4) -> (rule2 % int2)) triple4) -> (rule8 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
triple2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple3
Charlie is red.
("Charlie" "is" "red" "+")
triple4
Dave is nice.
("Dave" "is" "nice" "+")
triple5
Dave is quiet.
("Dave" "is" "quiet" "+")
triple6
Dave is young.
("Dave" "is" "young" "+")
triple7
Fiona is nice.
("Fiona" "is" "nice" "+")
triple8
Fiona is smart.
("Fiona" "is" "smart" "+")
triple9
Harry is big.
("Harry" "is" "big" "+")
triple10
Harry is quiet.
("Harry" "is" "quiet" "+")
triple11
((triple12 ((triple12) -> (rule1 % int2))) -> (rule3 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
triple12
Charlie is nice.
("Charlie" "is" "nice" "+")
((triple4) -> (rule2 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
((triple5 triple7) -> (rule5 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
((triple9) -> (rule1 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
((triple12) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
((((triple5 triple7) -> (rule5 % int2))) -> (rule6 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
((triple5 ((triple5 triple7) -> (rule5 % int2))) -> (rule8 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((triple9 ((triple9) -> (rule1 % int2))) -> (rule3 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
((((triple9 ((triple9) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
int3
Fiona is red.
("Fiona" "is" "red" "+")
((triple8 ((((triple9 ((triple9) -> (rule1 % int4))) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
Fiona is furry.
("Fiona" "is" "furry" "+")
int4
Fiona is big.
("Fiona" "is" "big" "+")
((((triple8 ((((triple9 ((triple9) -> (rule1 % int5))) -> (rule3 % int4))) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int4
Fiona is furry.
("Fiona" "is" "furry" "+")
int5
((triple8 ((triple8 ((((triple9 ((triple9) -> (rule1 % int5))) -> (rule3 % int4))) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int4
Fiona is furry.
("Fiona" "is" "furry" "+")
int5