Charlie is big. Dave is big. Dave is rough. Dave is round. Dave is smart. Dave is not young. Erin is big. Harry is big. Harry is furry. Harry is young. All big things are smart. If Harry is smart and Harry is not big then Harry is not furry. If something is furry and not smart then it is not young. Blue, young things are round. All young, smart things are not round. If something is smart and not round then it is rough.
Charlie is big.
("Charlie" "is" "big" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is not young.
("Dave" "is" "young" "-")
Erin is big.
("Erin" "is" "big" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is young.
("Harry" "is" "young" "+")
All big things are smart.
((("something" "is" "big" "+")) -> ("something" "is" "smart" "+"))
If Harry is smart and Harry is not big then Harry is not furry.
((("Harry" "is" "smart" "+") ("Harry" "is" "big" "~")) -> ("Harry" "is" "furry" "-"))
If something is furry and not smart then it is not young.
((("something" "is" "furry" "+") ("something" "is" "smart" "~")) -> ("something" "is" "young" "-"))
Blue, young things are round.
((("something" "is" "blue" "+") ("something" "is" "young" "+")) -> ("something" "is" "round" "+"))
All young, smart things are not round.
((("something" "is" "young" "+") ("something" "is" "smart" "+")) -> ("something" "is" "round" "-"))
If something is smart and not round then it is rough.
((("something" "is" "smart" "+") ("something" "is" "round" "~")) -> ("something" "is" "rough" "+"))
Harry is big.
True
1
proof
[(triple8)]
("Harry" "is" "big" "+")
triple8
Dave is not rough.
False
1
inv-proof
[(triple3)]
("Dave" "is" "rough" "-")
triple3
Erin is smart.
True
2
proof
[(((triple7) -> rule1))]
("Erin" "is" "smart" "+")
((triple7) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Harry is not smart.
False
2
inv-proof
[(((triple8) -> rule1))]
("Harry" "is" "smart" "-")
((triple8) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is not round.
True
4
proof
[(((triple10 ((triple8) -> rule1)) -> rule5))]
("Harry" "is" "round" "-")
((triple10 ((triple8) -> (rule1 % int2))) -> (rule5 % int1))
Harry is not round.
("Harry" "is" "round" "-")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is round.
False
4
inv-proof
[(((triple10 ((triple8) -> rule1)) -> rule5))]
("Harry" "is" "round" "+")
((triple10 ((triple8) -> (rule1 % int2))) -> (rule5 % int1))
Harry is not round.
("Harry" "is" "round" "-")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is rough.
True
7
proof
[(((((triple8) -> rule1) ((triple10 ((triple8) -> rule1)) -> rule5)) -> rule6))]
("Harry" "is" "rough" "+")
((((triple8) -> (rule1 % int3)) ((triple10 ((triple8) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is not round.
("Harry" "is" "round" "-")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
Harry is not rough.
False
7
inv-proof
[(((((triple8) -> rule1) ((triple10 ((triple8) -> rule1)) -> rule5)) -> rule6))]
("Harry" "is" "rough" "-")
((((triple8) -> (rule1 % int3)) ((triple10 ((triple8) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is not round.
("Harry" "is" "round" "-")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
Erin is not rough.
Unknown
inv-rconc
[@1: Erin is rough.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Erin" "is" "rough" "-")
Erin is round.
Unknown
rconc
[@1: Erin is round.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Erin" "is" "round" "+")
Charlie is not rough.
Unknown
inv-rconc
[@1: Charlie is rough.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "rough" "-")
Charlie is round.
Unknown
rconc
[@1: Charlie is round.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Charlie" "is" "round" "+")
Dave is not blue.
Unknown
inv-random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "-")
Erin is young.
Unknown
random
[@0: Erin is young.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "young" "+")
Charlie is not young.
Unknown
inv-random
[@0: Charlie is young.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "young" "-")
Harry is blue.
Unknown
random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "+")
@0: Charlie is big.[(triple1)] Dave is big.[(triple2)] Dave is not young.[(triple6)] Dave is rough.[(triple3)] Dave is round.[(triple4)] Dave is smart.[(triple5 OR ((triple2) -> rule1))] Erin is big.[(triple7)] Harry is big.[(triple8)] Harry is furry.[(triple9)] Harry is young.[(triple10)] @1: Charlie is smart.[(((triple1) -> rule1))] Erin is smart.[(((triple7) -> rule1))] Harry is smart.[(((triple8) -> rule1))] @2: Harry is not round.[(((triple10 ((triple8) -> rule1)) -> rule5))] @3: Harry is rough.[(((((triple8) -> rule1) ((triple10 ((triple8) -> rule1)) -> rule5)) -> rule6))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Dave is big.
("Dave" "is" "big" "+")
triple2
Dave is not young.
("Dave" "is" "young" "-")
triple6
Dave is rough.
("Dave" "is" "rough" "+")
triple3
Dave is round.
("Dave" "is" "round" "+")
triple4
Dave is smart.
("Dave" "is" "smart" "+")
triple5
((triple2) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
triple7
Harry is big.
("Harry" "is" "big" "+")
triple8
Harry is furry.
("Harry" "is" "furry" "+")
triple9
Harry is young.
("Harry" "is" "young" "+")
triple10
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple1) -> (rule1 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
((triple7) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
((triple8) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is not round.
("Harry" "is" "round" "-")
((triple10 ((triple8) -> (rule1 % int2))) -> (rule5 % int1))
Harry is not round.
("Harry" "is" "round" "-")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
((((triple8) -> (rule1 % int3)) ((triple10 ((triple8) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is not round.
("Harry" "is" "round" "-")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3