Bob is smart. Charlie is round. Dave is big. Dave is furry. Dave is not round. Erin is not blue. Erin is furry. Round, big people are white. All blue people are young. All blue people are young. All white people are young. Young, big people are blue. If someone is smart then they are round. All round people are big. If someone is round then they are smart.
Bob is smart.
("Bob" "is" "smart" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is not round.
("Dave" "is" "round" "-")
Erin is not blue.
("Erin" "is" "blue" "-")
Erin is furry.
("Erin" "is" "furry" "+")
Round, big people are white.
((("someone" "is" "round" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "white" "+"))
All blue people are young.
((("someone" "is" "blue" "+")) -> ("someone" "is" "young" "+"))
All blue people are young.
((("someone" "is" "blue" "+")) -> ("someone" "is" "young" "+"))
All white people are young.
((("someone" "is" "white" "+")) -> ("someone" "is" "young" "+"))
Young, big people are blue.
((("someone" "is" "young" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "blue" "+"))
If someone is smart then they are round.
((("someone" "is" "smart" "+")) -> ("someone" "is" "round" "+"))
All round people are big.
((("someone" "is" "round" "+")) -> ("someone" "is" "big" "+"))
If someone is round then they are smart.
((("someone" "is" "round" "+")) -> ("someone" "is" "smart" "+"))
Erin is furry.
True
1
proof
[(triple7)]
("Erin" "is" "furry" "+")
triple7
Charlie is not round.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "round" "-")
triple2
Charlie is smart.
True
2
proof
[(((triple2) -> rule8))]
("Charlie" "is" "smart" "+")
((triple2) -> (rule8 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is not big.
False
2
inv-proof
[(((triple2) -> rule7))]
("Charlie" "is" "big" "-")
((triple2) -> (rule7 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Bob is big.
True
3
proof
[(((((triple1) -> rule6)) -> rule7))]
("Bob" "is" "big" "+")
((((triple1) -> (rule6 % int2))) -> (rule7 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Charlie is not white.
False
4
inv-proof
[(((triple2 ((triple2) -> rule7)) -> rule1))]
("Charlie" "is" "white" "-")
((triple2 ((triple2) -> (rule7 % int2))) -> (rule1 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Bob is white.
True
6
proof
[(((((triple1) -> rule6) ((((triple1) -> rule6)) -> rule7)) -> rule1))]
("Bob" "is" "white" "+")
((((triple1) -> (rule6 % int3)) ((((triple1) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Charlie is not young.
False
5
inv-proof
[(((((triple2 ((triple2) -> rule7)) -> rule1)) -> rule4))]
("Charlie" "is" "young" "-")
((((triple2 ((triple2) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Charlie is blue.
True
8
proof
[(((((((triple2 ((triple2) -> rule7)) -> rule1)) -> rule4) ((triple2) -> rule7)) -> rule5))]
("Charlie" "is" "blue" "+")
((((((triple2 ((triple2) -> (rule7 % int4))) -> (rule1 % int3))) -> (rule4 % int2)) ((triple2) -> (rule7 % int4))) -> (rule5 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Charlie is big.
("Charlie" "is" "big" "+")
int4
Bob is not young.
False
7
inv-proof
[(((((((triple1) -> rule6) ((((triple1) -> rule6)) -> rule7)) -> rule1)) -> rule4))]
("Bob" "is" "young" "-")
((((((triple1) -> (rule6 % int4)) ((((triple1) -> (rule6 % int4))) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is round.
("Bob" "is" "round" "+")
int4
Bob is blue.
True
11
proof
[(((((((((triple1) -> rule6) ((((triple1) -> rule6)) -> rule7)) -> rule1)) -> rule4) ((((triple1) -> rule6)) -> rule7)) -> rule5))]
("Bob" "is" "blue" "+")
((((((((triple1) -> (rule6 % int5)) ((((triple1) -> (rule6 % int5))) -> (rule7 % int4))) -> (rule1 % int3))) -> (rule4 % int2)) ((((triple1) -> (rule6 % int5))) -> (rule7 % int4))) -> (rule5 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is big.
("Bob" "is" "big" "+")
int4
Bob is round.
("Bob" "is" "round" "+")
int5
Bob is not blue.
False
11
inv-proof
[(((((((((triple1) -> rule6) ((((triple1) -> rule6)) -> rule7)) -> rule1)) -> rule4) ((((triple1) -> rule6)) -> rule7)) -> rule5))]
("Bob" "is" "blue" "-")
((((((((triple1) -> (rule6 % int5)) ((((triple1) -> (rule6 % int5))) -> (rule7 % int4))) -> (rule1 % int3))) -> (rule4 % int2)) ((((triple1) -> (rule6 % int5))) -> (rule7 % int4))) -> (rule5 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is big.
("Bob" "is" "big" "+")
int4
Bob is round.
("Bob" "is" "round" "+")
int5
Erin is not white.
Unknown
inv-rconc
[@3: Erin is white.[CWA. Example of deepest failure = (rule1 <- rule6 <- rule8 <- FAIL)]]
("Erin" "is" "white" "-")
Erin is young.
Unknown
rconc
[@4: Erin is young.[CWA. Example of deepest failure = (rule4 <- rule1 <- rule6 <- rule8 <- FAIL)]]
("Erin" "is" "young" "+")
Erin is not smart.
Unknown
inv-rconc
[@2: Erin is smart.[CWA. Example of deepest failure = (rule8 <- rule6 <- FAIL)]]
("Erin" "is" "smart" "-")
Dave is white.
Unknown
rconc
[@1: Dave is white.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "white" "+")
Erin is not big.
Unknown
inv-rconc
[@3: Erin is big.[CWA. Example of deepest failure = (rule7 <- rule6 <- rule8 <- FAIL)]]
("Erin" "is" "big" "-")
Dave is young.
Unknown
rconc
[@4: Dave is young.[CWA. Example of deepest failure = (rule2 <- rule5 <- rule4 <- rule1 <- FAIL)]]
("Dave" "is" "young" "+")
Bob is not furry.
Unknown
inv-random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "-")
Charlie is furry.
Unknown
random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "+")
@0: Bob is smart.[(triple1)] Charlie is round.[(triple2)] Dave is big.[(triple3)] Dave is furry.[(triple4)] Dave is not round.[(triple5)] Erin is furry.[(triple7)] Erin is not blue.[(triple6)] @1: Bob is round.[(((triple1) -> rule6))] Charlie is big.[(((triple2) -> rule7))] Charlie is smart.[(((triple2) -> rule8))] @2: Bob is big.[(((((triple1) -> rule6)) -> rule7))] Charlie is white.[(((triple2 ((triple2) -> rule7)) -> rule1))] @3: Bob is white.[(((((triple1) -> rule6) ((((triple1) -> rule6)) -> rule7)) -> rule1))] Charlie is young.[(((((triple2 ((triple2) -> rule7)) -> rule1)) -> rule4))] @4: Bob is young.[(((((((triple1) -> rule6) ((((triple1) -> rule6)) -> rule7)) -> rule1)) -> rule4))] Charlie is blue.[(((((((triple2 ((triple2) -> rule7)) -> rule1)) -> rule4) ((triple2) -> rule7)) -> rule5))] @5: Bob is blue.[(((((((((triple1) -> rule6) ((((triple1) -> rule6)) -> rule7)) -> rule1)) -> rule4) ((((triple1) -> rule6)) -> rule7)) -> rule5))]
Bob is smart.
("Bob" "is" "smart" "+")
triple1
Charlie is round.
("Charlie" "is" "round" "+")
triple2
Dave is big.
("Dave" "is" "big" "+")
triple3
Dave is furry.
("Dave" "is" "furry" "+")
triple4
Dave is not round.
("Dave" "is" "round" "-")
triple5
Erin is furry.
("Erin" "is" "furry" "+")
triple7
Erin is not blue.
("Erin" "is" "blue" "-")
triple6
Bob is round.
("Bob" "is" "round" "+")
((triple1) -> (rule6 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
((triple2) -> (rule7 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple2) -> (rule8 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
((((triple1) -> (rule6 % int2))) -> (rule7 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
((triple2 ((triple2) -> (rule7 % int2))) -> (rule1 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
((((triple1) -> (rule6 % int3)) ((((triple1) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Charlie is young.
("Charlie" "is" "young" "+")
((((triple2 ((triple2) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Bob is young.
("Bob" "is" "young" "+")
((((((triple1) -> (rule6 % int4)) ((((triple1) -> (rule6 % int4))) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is round.
("Bob" "is" "round" "+")
int4
Charlie is blue.
("Charlie" "is" "blue" "+")
((((((triple2 ((triple2) -> (rule7 % int4))) -> (rule1 % int3))) -> (rule4 % int2)) ((triple2) -> (rule7 % int4))) -> (rule5 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Charlie is big.
("Charlie" "is" "big" "+")
int4
Bob is blue.
("Bob" "is" "blue" "+")
((((((((triple1) -> (rule6 % int5)) ((((triple1) -> (rule6 % int5))) -> (rule7 % int4))) -> (rule1 % int3))) -> (rule4 % int2)) ((((triple1) -> (rule6 % int5))) -> (rule7 % int4))) -> (rule5 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is big.
("Bob" "is" "big" "+")
int4
Bob is round.
("Bob" "is" "round" "+")
int5