Bob is cold. Bob is round. Erin is smart. Erin is white. Erin is young. Fiona is cold. Fiona is quiet. Fiona is not round. Fiona is white. Harry is cold. Harry is round. Harry is white. If Bob is cold and Bob is round then Bob is not white. If someone is quiet then they are young. All young people are smart. Young people are quiet. If someone is round and not white then they are quiet. If someone is white and not quiet then they are not big. All smart, quiet people are big. If Harry is big then Harry is cold.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is round.
("Bob" "is" "round" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is white.
("Erin" "is" "white" "+")
Erin is young.
("Erin" "is" "young" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is not round.
("Fiona" "is" "round" "-")
Fiona is white.
("Fiona" "is" "white" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is white.
("Harry" "is" "white" "+")
If Bob is cold and Bob is round then Bob is not white.
((("Bob" "is" "cold" "+") ("Bob" "is" "round" "+")) -> ("Bob" "is" "white" "-"))
If someone is quiet then they are young.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "young" "+"))
All young people are smart.
((("someone" "is" "young" "+")) -> ("someone" "is" "smart" "+"))
Young people are quiet.
((("someone" "is" "young" "+")) -> ("someone" "is" "quiet" "+"))
If someone is round and not white then they are quiet.
((("someone" "is" "round" "+") ("someone" "is" "white" "~")) -> ("someone" "is" "quiet" "+"))
If someone is white and not quiet then they are not big.
((("someone" "is" "white" "+") ("someone" "is" "quiet" "~")) -> ("someone" "is" "big" "-"))
All smart, quiet people are big.
((("someone" "is" "smart" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "big" "+"))
If Harry is big then Harry is cold.
((("Harry" "is" "big" "+")) -> ("Harry" "is" "cold" "+"))
Harry is round.
True
1
proof
[(triple11)]
("Harry" "is" "round" "+")
triple11
Fiona is not quiet.
False
1
inv-proof
[(triple7)]
("Fiona" "is" "quiet" "-")
triple7
Fiona is young.
True
2
proof
[(((triple7) -> rule2))]
("Fiona" "is" "young" "+")
((triple7) -> (rule2 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is not young.
False
2
inv-proof
[(((triple7) -> rule2))]
("Fiona" "is" "young" "-")
((triple7) -> (rule2 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is smart.
True
3
proof
[(((((triple7) -> rule2)) -> rule3))]
("Fiona" "is" "smart" "+")
((((triple7) -> (rule2 % int2))) -> (rule3 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Erin is not big.
False
4
inv-proof
[(((triple3 ((triple5) -> rule4)) -> rule7) OR ((((triple5) -> rule3) ((triple5) -> rule4)) -> rule7))]
("Erin" "is" "big" "-")
((triple3 ((triple5) -> (rule4 % int2))) -> (rule7 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
((((triple5) -> (rule3 % int3)) ((triple5) -> (rule4 % int2))) -> (rule7 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Fiona is big.
True
5
proof
[(((((((triple7) -> rule2)) -> rule3) triple7) -> rule7))]
("Fiona" "is" "big" "+")
((((((triple7) -> (rule2 % int3))) -> (rule3 % int2)) triple7) -> (rule7 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Fiona is not big.
False
5
inv-proof
[(((((((triple7) -> rule2)) -> rule3) triple7) -> rule7))]
("Fiona" "is" "big" "-")
((((((triple7) -> (rule2 % int3))) -> (rule3 % int2)) triple7) -> (rule7 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Bob is smart.
True
7
proof
[(((((((triple2 ((triple1 triple2) -> rule1)) -> rule5)) -> rule2)) -> rule3))]
("Bob" "is" "smart" "+")
((((((triple2 ((triple1 triple2) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is not white.
("Bob" "is" "white" "-")
int4
Bob is not smart.
False
7
inv-proof
[(((((((triple2 ((triple1 triple2) -> rule1)) -> rule5)) -> rule2)) -> rule3))]
("Bob" "is" "smart" "-")
((((((triple2 ((triple1 triple2) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is not white.
("Bob" "is" "white" "-")
int4
Bob is big.
True
13
proof
[(((((((((triple2 ((triple1 triple2) -> rule1)) -> rule5)) -> rule2)) -> rule3) ((triple2 ((triple1 triple2) -> rule1)) -> rule5)) -> rule7))]
("Bob" "is" "big" "+")
((((((((triple2 ((triple1 triple2) -> (rule1 % int5))) -> (rule5 % int4))) -> (rule2 % int3))) -> (rule3 % int2)) ((triple2 ((triple1 triple2) -> (rule1 % int5))) -> (rule5 % int4))) -> (rule7 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is quiet.
("Bob" "is" "quiet" "+")
int4
Bob is not white.
("Bob" "is" "white" "-")
int5
Bob is not big.
False
13
inv-proof
[(((((((((triple2 ((triple1 triple2) -> rule1)) -> rule5)) -> rule2)) -> rule3) ((triple2 ((triple1 triple2) -> rule1)) -> rule5)) -> rule7))]
("Bob" "is" "big" "-")
((((((((triple2 ((triple1 triple2) -> (rule1 % int5))) -> (rule5 % int4))) -> (rule2 % int3))) -> (rule3 % int2)) ((triple2 ((triple1 triple2) -> (rule1 % int5))) -> (rule5 % int4))) -> (rule7 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is quiet.
("Bob" "is" "quiet" "+")
int4
Bob is not white.
("Bob" "is" "white" "-")
int5
Harry is not smart.
Unknown
inv-rconc
[@3: Harry is smart.[CWA. Example of deepest failure = (rule3 <- rule2 <- rule4 <- FAIL)]]
("Harry" "is" "smart" "-")
Harry is big.
Unknown
rconc
[@4: Harry is big.[CWA. Example of deepest failure = (rule7 <- rule3 <- rule2 <- rule4 <- FAIL)]]
("Harry" "is" "big" "+")
Harry is not quiet.
Unknown
inv-rconc
[@3: Harry is quiet.[CWA. Example of deepest failure = (rule4 <- rule2 <- rule5 <- FAIL)]]
("Harry" "is" "quiet" "-")
Harry is young.
Unknown
rconc
[@2: Harry is young.[CWA. Example of deepest failure = (rule2 <- rule4 <- FAIL)]]
("Harry" "is" "young" "+")
Erin is not cold.
Unknown
inv-random
[@0: Erin is cold.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "cold" "-")
Erin is round.
Unknown
random
[@0: Erin is round.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "round" "+")
@0: Bob is cold.[(triple1)] Bob is round.[(triple2)] Erin is smart.[(triple3 OR ((triple5) -> rule3))] Erin is white.[(triple4)] Erin is young.[(triple5)] Fiona is cold.[(triple6)] Fiona is not round.[(triple8)] Fiona is quiet.[(triple7)] Fiona is white.[(triple9)] Harry is cold.[(triple10)] Harry is round.[(triple11)] Harry is white.[(triple12)] @1: Bob is not white.[(((triple1 triple2) -> rule1))] Erin is quiet.[(((triple5) -> rule4))] Fiona is young.[(((triple7) -> rule2))] @2: Bob is quiet.[(((triple2 ((triple1 triple2) -> rule1)) -> rule5))] Erin is big.[(((triple3 ((triple5) -> rule4)) -> rule7) OR ((((triple5) -> rule3) ((triple5) -> rule4)) -> rule7))] Fiona is smart.[(((((triple7) -> rule2)) -> rule3))] @3: Bob is young.[(((((triple2 ((triple1 triple2) -> rule1)) -> rule5)) -> rule2))] Fiona is big.[(((((((triple7) -> rule2)) -> rule3) triple7) -> rule7))] @4: Bob is smart.[(((((((triple2 ((triple1 triple2) -> rule1)) -> rule5)) -> rule2)) -> rule3))] @5: Bob is big.[(((((((((triple2 ((triple1 triple2) -> rule1)) -> rule5)) -> rule2)) -> rule3) ((triple2 ((triple1 triple2) -> rule1)) -> rule5)) -> rule7))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Bob is round.
("Bob" "is" "round" "+")
triple2
Erin is smart.
("Erin" "is" "smart" "+")
triple3
((triple5) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
triple4
Erin is young.
("Erin" "is" "young" "+")
triple5
Fiona is cold.
("Fiona" "is" "cold" "+")
triple6
Fiona is not round.
("Fiona" "is" "round" "-")
triple8
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple7
Fiona is white.
("Fiona" "is" "white" "+")
triple9
Harry is cold.
("Harry" "is" "cold" "+")
triple10
Harry is round.
("Harry" "is" "round" "+")
triple11
Harry is white.
("Harry" "is" "white" "+")
triple12
Bob is not white.
("Bob" "is" "white" "-")
((triple1 triple2) -> (rule1 % int1))
Bob is not white.
("Bob" "is" "white" "-")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
((triple5) -> (rule4 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
((triple7) -> (rule2 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
((triple2 ((triple1 triple2) -> (rule1 % int2))) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is not white.
("Bob" "is" "white" "-")
int2
Erin is big.
("Erin" "is" "big" "+")
((triple3 ((triple5) -> (rule4 % int2))) -> (rule7 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
((((triple5) -> (rule3 % int3)) ((triple5) -> (rule4 % int2))) -> (rule7 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Fiona is smart.
("Fiona" "is" "smart" "+")
((((triple7) -> (rule2 % int2))) -> (rule3 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
((((triple2 ((triple1 triple2) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is not white.
("Bob" "is" "white" "-")
int3
Fiona is big.
("Fiona" "is" "big" "+")
((((((triple7) -> (rule2 % int3))) -> (rule3 % int2)) triple7) -> (rule7 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
((((((triple2 ((triple1 triple2) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is not white.
("Bob" "is" "white" "-")
int4
Bob is big.
("Bob" "is" "big" "+")
((((((((triple2 ((triple1 triple2) -> (rule1 % int5))) -> (rule5 % int4))) -> (rule2 % int3))) -> (rule3 % int2)) ((triple2 ((triple1 triple2) -> (rule1 % int5))) -> (rule5 % int4))) -> (rule7 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is quiet.
("Bob" "is" "quiet" "+")
int4
Bob is not white.
("Bob" "is" "white" "-")
int5